update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / ex1 / props.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/ex1/props.ma b/matita/matita/contribs/lambdadelta/basic_1/ex1/props.ma
index 5c442f5bb431285e31bce298bf2c86601a0dc472..91ce1745bcad69dfb68c1ba063bd5250ac6aa922 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/ex1/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/ex1/props.ma
@@ -14,31 +14,28 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/ex1/defs.ma".
+include "basic_1/ex1/defs.ma".
 
-include "Basic-1/ty3/fwd.ma".
+include "basic_1/ty3/fwd.ma".
 
-include "Basic-1/pc3/fwd.ma".
+include "basic_1/pc3/fwd.ma".
 
-include "Basic-1/nf2/pr3.ma".
+include "basic_1/nf2/pr3.ma".
 
-include "Basic-1/nf2/props.ma".
+include "basic_1/nf2/props.ma".
 
-include "Basic-1/arity/defs.ma".
+include "basic_1/arity/defs.ma".
 
-include "Basic-1/leq/props.ma".
+include "basic_1/leq/props.ma".
 
-theorem ex1__leq_sort_SS:
+fact ex1__leq_sort_SS:
  \forall (g: G).(\forall (k: nat).(\forall (n: nat).(leq g (ASort k n) (asucc 
 g (asucc g (ASort (S (S k)) n))))))
 \def
  \lambda (g: G).(\lambda (k: nat).(\lambda (n: nat).(leq_refl g (asucc g 
 (asucc g (ASort (S (S k)) n)))))).
-(* COMMENTS
-Initial nodes: 27
-END *)
 
-theorem ex1_arity:
+lemma ex1_arity:
  \forall (g: G).(arity g ex1_c ex1_t (ASort O O))
 \def
  \lambda (g: G).(arity_appl g (CHead (CHead (CHead (CSort O) (Bind Abst) 
@@ -69,11 +66,8 @@ O) (ASort O O) (arity_sort g (CSort O) O) (asucc g (asucc g (ASort (S (S O))
 O))) (ex1__leq_sort_SS g O O))) (TSort O) (ASort O O) (arity_sort g (CHead 
 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
 (Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) O))).
-(* COMMENTS
-Initial nodes: 753
-END *)
 
-theorem ex1_ty3:
+lemma ex1_ty3:
  \forall (g: G).(\forall (u: T).((ty3 g ex1_c ex1_t u) \to (\forall (P: 
 Prop).P)))
 \def
@@ -179,137 +173,133 @@ e)) (\lambda (e: C).(clear e (CHead x7 (Bind Abbr) x8))) P (\lambda (x:
 C).(\lambda (_: (drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
 (Bind Abst) (TSort O)) x)).(\lambda (_: (clear x (CHead x7 (Bind Abbr) 
 x8))).(let H17 \def (eq_ind C (CHead x2 (Bind Abbr) x3) (\lambda (ee: 
-C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow 
-False | (CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop) 
-with [(Bind b) \Rightarrow (match b in B return (\lambda (_: B).Prop) with 
-[Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False]) | 
-(Flat _) \Rightarrow False])])) I (CHead (CHead (CHead (CSort O) (Bind Abst) 
-(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (clear_gen_bind Abst 
+C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow 
+(match k with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow True | 
+Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _) \Rightarrow 
+False])])) I (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x2 (Bind Abbr) 
+x3) (TLRef O) (getl_gen_O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abbr) x3) 
+H5))) in (False_ind P H17))))) H14)))))))) H10)) (\lambda (H10: (ex3_3 C T T 
+(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (lift (S (S (S O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: 
+T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) 
+u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 
+t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: 
+T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) x6)))) (\lambda 
+(e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
+(t: T).(ty3 g e u0 t)))) P (\lambda (x7: C).(\lambda (x8: T).(\lambda (x9: 
+T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O x8) 
+x6)).(\lambda (H12: (getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x7 
+(Bind Abst) x8))).(\lambda (_: (ty3 g x7 x8 x9)).(let H14 \def (getl_gen_all 
 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead 
-x2 (Bind Abbr) x3) (TLRef O) (getl_gen_O (CHead (CHead (CHead (CSort O) (Bind 
-Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 
-(Bind Abbr) x3) H5))) in (False_ind P H17))))) H14)))))))) H10)) (\lambda 
-(H10: (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 
+x7 (Bind Abst) x8) (r (Bind Abst) (S O)) (getl_gen_S (Bind Abst) (CHead 
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x7 
+(Bind Abst) x8) (TLRef O) (S O) H12)) in (ex2_ind C (\lambda (e: C).(drop (S 
+O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+e)) (\lambda (e: C).(clear e (CHead x7 (Bind Abst) x8))) P (\lambda (x: 
+C).(\lambda (_: (drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) x)).(\lambda (_: (clear x (CHead x7 (Bind Abst) 
+x8))).(let H17 \def (eq_ind C (CHead x2 (Bind Abbr) x3) (\lambda (ee: 
+C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow 
+(match k with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow True | 
+Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _) \Rightarrow 
+False])])) I (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x2 (Bind Abbr) 
+x3) (TLRef O) (getl_gen_O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abbr) x3) 
+H5))) in (False_ind P H17))))) H14)))))))) H10)) (ty3_gen_lref g (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) x6 (S (S O)) H8))))))) (ty3_gen_bind g Abst (CHead (CHead 
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) 
+(TLRef O)) (TLRef (S (S O))) (TSort O) (THead (Bind Abst) x0 x1) H1)))))))) 
+H3)) (\lambda (H3: (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: 
+T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O u0) x0)))) (\lambda (e: 
+C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e 
+(Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e 
+u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: 
+T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O u0) x0)))) (\lambda (e: 
+C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e 
+(Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e 
+u0 t)))) P (\lambda (x2: C).(\lambda (x3: T).(\lambda (x4: T).(\lambda (H4: 
+(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort 
+O)) (Bind Abst) (TLRef O)) (lift (S O) O x3) x0)).(\lambda (H5: (getl O 
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O)) (CHead x2 (Bind Abst) x3))).(\lambda (H6: (ty3 g x2 x3 
+x4)).(ex3_2_ind T T (\lambda (t2: T).(\lambda (_: T).(pc3 (CHead (CHead 
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) 
+(TLRef O)) (THead (Bind Abst) (TLRef (S (S O))) t2) (THead (Bind Abst) x0 
+x1)))) (\lambda (_: T).(\lambda (t: T).(ty3 g (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef 
+(S (S O))) t))) (\lambda (t2: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead 
+(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) 
+(TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort O) t2))) P (\lambda (x5: 
+T).(\lambda (x6: T).(\lambda (H7: (pc3 (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind 
+Abst) (TLRef (S (S O))) x5) (THead (Bind Abst) x0 x1))).(\lambda (H8: (ty3 g 
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O)) (TLRef (S (S O))) x6)).(\lambda (_: (ty3 g (CHead 
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort O) x5)).(or_ind 
+(ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) (\lambda (e: C).(\lambda 
+(u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind 
+Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 
+t))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 
 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
 (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) x6)))) (\lambda (e: 
 C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead 
 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
 O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
-(t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u0: 
-T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
-(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) 
-x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) 
-(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
-(Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda 
-(u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x7: C).(\lambda (x8: 
-T).(\lambda (x9: T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind 
+(t: T).(ty3 g e u0 t))))) P (\lambda (H10: (ex3_3 C T T (\lambda (_: 
+C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind 
 Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S 
-O))) O x8) x6)).(\lambda (H12: (getl (S (S O)) (CHead (CHead (CHead (CSort O) 
-(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead 
-x7 (Bind Abst) x8))).(\lambda (_: (ty3 g x7 x8 x9)).(let H14 \def 
-(getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
-(TSort O)) (CHead x7 (Bind Abst) x8) (r (Bind Abst) (S O)) (getl_gen_S (Bind 
-Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
-(CHead x7 (Bind Abst) x8) (TLRef O) (S O) H12)) in (ex2_ind C (\lambda (e: 
-C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
-(TSort O)) e)) (\lambda (e: C).(clear e (CHead x7 (Bind Abst) x8))) P 
-(\lambda (x: C).(\lambda (_: (drop (S O) O (CHead (CHead (CSort O) (Bind 
-Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (_: (clear x (CHead x7 
-(Bind Abst) x8))).(let H17 \def (eq_ind C (CHead x2 (Bind Abbr) x3) (\lambda 
-(ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) 
-\Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda 
-(_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_: 
-B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void 
-\Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CHead (CHead 
-(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
-O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
-Abst) (TSort O)) (CHead x2 (Bind Abbr) x3) (TLRef O) (getl_gen_O (CHead 
-(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
-Abst) (TLRef O)) (CHead x2 (Bind Abbr) x3) H5))) in (False_ind P H17))))) 
-H14)))))))) H10)) (ty3_gen_lref g (CHead (CHead (CHead (CSort O) (Bind Abst) 
-(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) x6 (S (S O)) 
-H8))))))) (ty3_gen_bind g Abst (CHead (CHead (CHead (CSort O) (Bind Abst) 
-(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) 
-(TSort O) (THead (Bind Abst) x0 x1) H1)))))))) H3)) (\lambda (H3: (ex3_3 C T 
-T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead 
-(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
-O)) (lift (S O) O u0) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: 
-T).(getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
-(TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: 
+O))) O t) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S 
+O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort 
+O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: 
 C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T 
-(\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead 
-(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
-O)) (lift (S O) O u0) x0)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: 
-T).(getl O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
-(TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: 
-C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x2: 
-C).(\lambda (x3: T).(\lambda (x4: T).(\lambda (H4: (pc3 (CHead (CHead (CHead 
-(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
-O)) (lift (S O) O x3) x0)).(\lambda (H5: (getl O (CHead (CHead (CHead (CSort 
-O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
-(CHead x2 (Bind Abst) x3))).(\lambda (H6: (ty3 g x2 x3 x4)).(ex3_2_ind T T 
-(\lambda (t2: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind 
-Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind 
-Abst) (TLRef (S (S O))) t2) (THead (Bind Abst) x0 x1)))) (\lambda (_: 
-T).(\lambda (t: T).(ty3 g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort 
-O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) t))) 
-(\lambda (t2: T).(\lambda (_: T).(ty3 g (CHead (CHead (CHead (CHead (CSort O) 
-(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind 
-Abst) (TLRef (S (S O)))) (TSort O) t2))) P (\lambda (x5: T).(\lambda (x6: 
-T).(\lambda (H7: (pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
-(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (THead (Bind Abst) (TLRef (S (S 
-O))) x5) (THead (Bind Abst) x0 x1))).(\lambda (H8: (ty3 g (CHead (CHead 
-(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) 
-(TLRef O)) (TLRef (S (S O))) x6)).(\lambda (_: (ty3 g (CHead (CHead (CHead 
-(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) 
-(TLRef O)) (Bind Abst) (TLRef (S (S O)))) (TSort O) x5)).(or_ind (ex3_3 C T T 
 (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CHead 
 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
 O)) (lift (S (S (S O))) O t) x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
 (_: T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
 (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) 
-(\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C 
-T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda 
+(x7: C).(\lambda (x8: T).(\lambda (x9: T).(\lambda (_: (pc3 (CHead (CHead 
 (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) 
-(TLRef O)) (lift (S (S (S O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: 
-T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) 
-(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) 
-u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P 
-(\lambda (H10: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: 
-T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
-(TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) (\lambda 
-(e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead 
-(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
-O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
-(t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_: 
-T).(\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
-(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)))) 
-(\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead 
-(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
-Abst) (TLRef O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: 
-T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x7: C).(\lambda (x8: 
-T).(\lambda (x9: T).(\lambda (_: (pc3 (CHead (CHead (CHead (CSort O) (Bind 
-Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S 
-O))) O x9) x6)).(\lambda (H12: (getl (S (S O)) (CHead (CHead (CHead (CSort O) 
-(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead 
-x7 (Bind Abbr) x8))).(\lambda (_: (ty3 g x7 x8 x9)).(let H14 \def 
-(getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
-(TSort O)) (CHead x7 (Bind Abbr) x8) (r (Bind Abst) (S O)) (getl_gen_S (Bind 
-Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
-(CHead x7 (Bind Abbr) x8) (TLRef O) (S O) H12)) in (ex2_ind C (\lambda (e: 
-C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
-(TSort O)) e)) (\lambda (e: C).(clear e (CHead x7 (Bind Abbr) x8))) P 
-(\lambda (x: C).(\lambda (H15: (drop (S O) O (CHead (CHead (CSort O) (Bind 
-Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (H16: (clear x (CHead x7 
-(Bind Abbr) x8))).(let H17 \def (f_equal C C (\lambda (e: C).(match e in C 
-return (\lambda (_: C).C) with [(CSort _) \Rightarrow x2 | (CHead c _ _) 
-\Rightarrow c])) (CHead x2 (Bind Abst) x3) (CHead (CHead (CHead (CSort O) 
-(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
-(clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
-Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O) (getl_gen_O (CHead 
-(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
-Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in ((let H18 \def (f_equal C 
-T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _) 
+(TLRef O)) (lift (S (S (S O))) O x9) x6)).(\lambda (H12: (getl (S (S O)) 
+(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(Bind Abst) (TLRef O)) (CHead x7 (Bind Abbr) x8))).(\lambda (_: (ty3 g x7 x8 
+x9)).(let H14 \def (getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (CHead x7 (Bind Abbr) x8) (r (Bind Abst) (S O)) 
+(getl_gen_S (Bind Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (CHead x7 (Bind Abbr) x8) (TLRef O) (S O) H12)) in (ex2_ind 
+C (\lambda (e: C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) e)) (\lambda (e: C).(clear e (CHead x7 (Bind Abbr) 
+x8))) P (\lambda (x: C).(\lambda (H15: (drop (S O) O (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (H16: (clear x 
+(CHead x7 (Bind Abbr) x8))).(let H17 \def (f_equal C C (\lambda (e: C).(match 
+e with [(CSort _) \Rightarrow x2 | (CHead c _ _) \Rightarrow c])) (CHead x2 
+(Bind Abst) x3) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
+Abst) (TSort O)) (Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x2 (Bind Abst) 
+x3) (TLRef O) (getl_gen_O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort 
+O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) 
+H5))) in ((let H18 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _) 
 \Rightarrow x3 | (CHead _ _ t) \Rightarrow t])) (CHead x2 (Bind Abst) x3) 
 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
 (Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind 
@@ -327,31 +317,30 @@ O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) H19) in (let H23 \def
 (CSort O) (Bind Abst) (TSort O)) (drop_gen_refl (CHead (CSort O) (Bind Abst) 
 (TSort O)) x (drop_gen_drop (Bind Abst) (CHead (CSort O) (Bind Abst) (TSort 
 O)) x (TSort O) O H15))) in (let H24 \def (eq_ind C (CHead x7 (Bind Abbr) x8) 
-(\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) 
-\Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda 
-(_: K).Prop) with [(Bind b) \Rightarrow (match b in B return (\lambda (_: 
-B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | Void 
-\Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CSort O) 
-(Bind Abst) (TSort O)) (clear_gen_bind Abst (CSort O) (CHead x7 (Bind Abbr) 
-x8) (TSort O) H23)) in (False_ind P H24)))))))) H17))))) H14)))))))) H10)) 
-(\lambda (H10: (ex3_3 C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: 
+(\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _) 
+\Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr 
+\Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat 
+_) \Rightarrow False])])) I (CHead (CSort O) (Bind Abst) (TSort O)) 
+(clear_gen_bind Abst (CSort O) (CHead x7 (Bind Abbr) x8) (TSort O) H23)) in 
+(False_ind P H24)))))))) H17))))) H14)))))))) H10)) (\lambda (H10: (ex3_3 C T 
+T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
+O)) (lift (S (S (S O))) O u0) x6)))) (\lambda (e: C).(\lambda (u0: 
+T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead e (Bind Abst) 
+u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 
+t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: 
 T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
 (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) x6)))) (\lambda 
 (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) (CHead (CHead (CHead 
 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef 
 O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
-(t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u0: 
-T).(\lambda (_: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
-(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O u0) 
-x6)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl (S (S O)) 
-(CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
-(Bind Abst) (TLRef O)) (CHead e (Bind Abst) u0))))) (\lambda (e: C).(\lambda 
-(u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x7: C).(\lambda (x8: 
-T).(\lambda (x9: T).(\lambda (H11: (pc3 (CHead (CHead (CHead (CSort O) (Bind 
-Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S 
-O))) O x8) x6)).(\lambda (H12: (getl (S (S O)) (CHead (CHead (CHead (CSort O) 
-(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead 
-x7 (Bind Abst) x8))).(\lambda (H13: (ty3 g x7 x8 x9)).(let H14 \def 
+(t: T).(ty3 g e u0 t)))) P (\lambda (x7: C).(\lambda (x8: T).(\lambda (x9: 
+T).(\lambda (H11: (pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O x8) 
+x6)).(\lambda (H12: (getl (S (S O)) (CHead (CHead (CHead (CSort O) (Bind 
+Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x7 
+(Bind Abst) x8))).(\lambda (H13: (ty3 g x7 x8 x9)).(let H14 \def 
 (getl_gen_all (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
 (TSort O)) (CHead x7 (Bind Abst) x8) (r (Bind Abst) (S O)) (getl_gen_S (Bind 
 Abst) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
@@ -360,15 +349,14 @@ C).(drop (S O) O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst)
 (TSort O)) e)) (\lambda (e: C).(clear e (CHead x7 (Bind Abst) x8))) P 
 (\lambda (x: C).(\lambda (H15: (drop (S O) O (CHead (CHead (CSort O) (Bind 
 Abst) (TSort O)) (Bind Abst) (TSort O)) x)).(\lambda (H16: (clear x (CHead x7 
-(Bind Abst) x8))).(let H17 \def (f_equal C C (\lambda (e: C).(match e in C 
-return (\lambda (_: C).C) with [(CSort _) \Rightarrow x2 | (CHead c _ _) 
-\Rightarrow c])) (CHead x2 (Bind Abst) x3) (CHead (CHead (CHead (CSort O) 
-(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
-(clear_gen_bind Abst (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
-Abst) (TSort O)) (CHead x2 (Bind Abst) x3) (TLRef O) (getl_gen_O (CHead 
-(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
-Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) in ((let H18 \def (f_equal C 
-T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _) 
+(Bind Abst) x8))).(let H17 \def (f_equal C C (\lambda (e: C).(match e with 
+[(CSort _) \Rightarrow x2 | (CHead c _ _) \Rightarrow c])) (CHead x2 (Bind 
+Abst) x3) (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
+(TSort O)) (Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x2 (Bind Abst) x3) 
+(TLRef O) (getl_gen_O (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
+(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (CHead x2 (Bind Abst) x3) H5))) 
+in ((let H18 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _) 
 \Rightarrow x3 | (CHead _ _ t) \Rightarrow t])) (CHead x2 (Bind Abst) x3) 
 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
 (Bind Abst) (TLRef O)) (clear_gen_bind Abst (CHead (CHead (CSort O) (Bind 
@@ -386,48 +374,46 @@ O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) H19) in (let H23 \def
 (CSort O) (Bind Abst) (TSort O)) (drop_gen_refl (CHead (CSort O) (Bind Abst) 
 (TSort O)) x (drop_gen_drop (Bind Abst) (CHead (CSort O) (Bind Abst) (TSort 
 O)) x (TSort O) O H15))) in (let H24 \def (f_equal C C (\lambda (e: C).(match 
-e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow x7 | (CHead c _ 
-_) \Rightarrow c])) (CHead x7 (Bind Abst) x8) (CHead (CSort O) (Bind Abst) 
-(TSort O)) (clear_gen_bind Abst (CSort O) (CHead x7 (Bind Abst) x8) (TSort O) 
-H23)) in ((let H25 \def (f_equal C T (\lambda (e: C).(match e in C return 
-(\lambda (_: C).T) with [(CSort _) \Rightarrow x8 | (CHead _ _ t) \Rightarrow 
-t])) (CHead x7 (Bind Abst) x8) (CHead (CSort O) (Bind Abst) (TSort O)) 
-(clear_gen_bind Abst (CSort O) (CHead x7 (Bind Abst) x8) (TSort O) H23)) in 
-(\lambda (H26: (eq C x7 (CSort O))).(let H27 \def (eq_ind T x8 (\lambda (t: 
-T).(ty3 g x7 t x9)) H13 (TSort O) H25) in (let H28 \def (eq_ind T x8 (\lambda 
-(t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
-(TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) O t) x6)) H11 (TSort O) 
-H25) in (let H29 \def (eq_ind C x7 (\lambda (c: C).(ty3 g c (TSort O) x9)) 
-H27 (CSort O) H26) in (or_ind (ex3_3 C T T (\lambda (_: C).(\lambda (_: 
+e with [(CSort _) \Rightarrow x7 | (CHead c _ _) \Rightarrow c])) (CHead x7 
+(Bind Abst) x8) (CHead (CSort O) (Bind Abst) (TSort O)) (clear_gen_bind Abst 
+(CSort O) (CHead x7 (Bind Abst) x8) (TSort O) H23)) in ((let H25 \def 
+(f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow x8 | (CHead 
+_ _ t) \Rightarrow t])) (CHead x7 (Bind Abst) x8) (CHead (CSort O) (Bind 
+Abst) (TSort O)) (clear_gen_bind Abst (CSort O) (CHead x7 (Bind Abst) x8) 
+(TSort O) H23)) in (\lambda (H26: (eq C x7 (CSort O))).(let H27 \def (eq_ind 
+T x8 (\lambda (t: T).(ty3 g x7 t x9)) H13 (TSort O) H25) in (let H28 \def 
+(eq_ind T x8 (\lambda (t: T).(pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S (S (S O))) 
+O t) x6)) H11 (TSort O) H25) in (let H29 \def (eq_ind C x7 (\lambda (c: 
+C).(ty3 g c (TSort O) x9)) H27 (CSort O) H26) in (or_ind (ex3_3 C T T 
+(\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O t) x4)))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abbr) u0))))) 
+(\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C 
+T T (\lambda (_: C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) 
+x4)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) 
+u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P 
+(\lambda (H30: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: 
+T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(lift (S O) O t) x4)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: 
+T).(getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort 
+O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda 
+(t: T).(ty3 g e u0 t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_: 
 T).(\lambda (t: T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
 Abst) (TSort O)) (lift (S O) O t) x4)))) (\lambda (e: C).(\lambda (u0: 
 T).(\lambda (_: T).(getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
 (Bind Abst) (TSort O)) (CHead e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda 
-(u0: T).(\lambda (t: T).(ty3 g e u0 t))))) (ex3_3 C T T (\lambda (_: 
-C).(\lambda (u0: T).(\lambda (_: T).(pc3 (CHead (CHead (CSort O) (Bind Abst) 
-(TSort O)) (Bind Abst) (TSort O)) (lift (S O) O u0) x4)))) (\lambda (e: 
-C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead (CHead (CSort O) (Bind 
-Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind Abst) u0))))) (\lambda 
-(e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 t))))) P (\lambda (H30: 
-(ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 (CHead 
-(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O 
-t) x4)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O (CHead 
-(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead e (Bind 
-Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g e u0 
-t)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(pc3 
-(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (lift 
-(S O) O t) x4)))) (\lambda (e: C).(\lambda (u0: T).(\lambda (_: T).(getl O 
-(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead 
-e (Bind Abbr) u0))))) (\lambda (e: C).(\lambda (u0: T).(\lambda (t: T).(ty3 g 
-e u0 t)))) P (\lambda (x10: C).(\lambda (x11: T).(\lambda (x12: T).(\lambda 
-(_: (pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort 
-O)) (lift (S O) O x12) x4)).(\lambda (H32: (getl O (CHead (CHead (CSort O) 
-(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x10 (Bind Abbr) 
-x11))).(\lambda (_: (ty3 g x10 x11 x12)).(let H34 \def (eq_ind C (CHead x10 
-(Bind Abbr) x11) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) 
-with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K 
-return (\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return 
-(\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False | 
+(u0: T).(\lambda (t: T).(ty3 g e u0 t)))) P (\lambda (x10: C).(\lambda (x11: 
+T).(\lambda (x12: T).(\lambda (_: (pc3 (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (lift (S O) O x12) x4)).(\lambda (H32: 
+(getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
+(CHead x10 (Bind Abbr) x11))).(\lambda (_: (ty3 g x10 x11 x12)).(let H34 \def 
+(eq_ind C (CHead x10 (Bind Abbr) x11) (\lambda (ee: C).(match ee with [(CSort 
+_) \Rightarrow False | (CHead _ k _) \Rightarrow (match k with [(Bind b) 
+\Rightarrow (match b with [Abbr \Rightarrow True | Abst \Rightarrow False | 
 Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead (CHead 
 (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (clear_gen_bind Abst 
 (CHead (CSort O) (Bind Abst) (TSort O)) (CHead x10 (Bind Abbr) x11) (TSort O) 
@@ -448,14 +434,13 @@ T).(\lambda (x12: T).(\lambda (H31: (pc3 (CHead (CHead (CSort O) (Bind Abst)
 (TSort O)) (Bind Abst) (TSort O)) (lift (S O) O x11) x4)).(\lambda (H32: 
 (getl O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
 (CHead x10 (Bind Abst) x11))).(\lambda (H33: (ty3 g x10 x11 x12)).(let H34 
-\def (f_equal C C (\lambda (e: C).(match e in C return (\lambda (_: C).C) 
-with [(CSort _) \Rightarrow x10 | (CHead c _ _) \Rightarrow c])) (CHead x10 
-(Bind Abst) x11) (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) 
-(TSort O)) (clear_gen_bind Abst (CHead (CSort O) (Bind Abst) (TSort O)) 
-(CHead x10 (Bind Abst) x11) (TSort O) (getl_gen_O (CHead (CHead (CSort O) 
-(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead x10 (Bind Abst) x11) 
-H32))) in ((let H35 \def (f_equal C T (\lambda (e: C).(match e in C return 
-(\lambda (_: C).T) with [(CSort _) \Rightarrow x11 | (CHead _ _ t) 
+\def (f_equal C C (\lambda (e: C).(match e with [(CSort _) \Rightarrow x10 | 
+(CHead c _ _) \Rightarrow c])) (CHead x10 (Bind Abst) x11) (CHead (CHead 
+(CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (clear_gen_bind Abst 
+(CHead (CSort O) (Bind Abst) (TSort O)) (CHead x10 (Bind Abst) x11) (TSort O) 
+(getl_gen_O (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort 
+O)) (CHead x10 (Bind Abst) x11) H32))) in ((let H35 \def (f_equal C T 
+(\lambda (e: C).(match e with [(CSort _) \Rightarrow x11 | (CHead _ _ t) 
 \Rightarrow t])) (CHead x10 (Bind Abst) x11) (CHead (CHead (CSort O) (Bind 
 Abst) (TSort O)) (Bind Abst) (TSort O)) (clear_gen_bind Abst (CHead (CSort O) 
 (Bind Abst) (TSort O)) (CHead x10 (Bind Abst) x11) (TSort O) (getl_gen_O 
@@ -483,7 +468,7 @@ Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) H40 (lift (S O) O
 O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (lift (S O) O (TLRef O))) 
 (pr3 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort 
 O)) (Bind Abst) (TLRef O)) x0) H21)) (TLRef (plus O (S O))) (lift_lref_ge O 
-(S O) O (le_n O))) in (let H43 \def H42 in (ex2_ind T (\lambda (t: T).(pr3 
+(S O) O (le_O_n O))) in (let H43 \def H42 in (ex2_ind T (\lambda (t: T).(pr3 
 (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
 (Bind Abst) (TLRef O)) (TLRef (S (S O))) t)) (\lambda (t: T).(pr3 (CHead 
 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
@@ -511,26 +496,21 @@ x13 H45 (nf2_lref_abst (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O))
 (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (CHead (CHead (CSort O) (Bind 
 Abst) (TSort O)) (Bind Abst) (TSort O)) (getl_refl Abst (CHead (CSort O) 
 (Bind Abst) (TSort O)) (TSort O)) (TLRef O))))) in (let H47 \def (eq_ind T 
-(TLRef (S (S O))) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef n) \Rightarrow (match n 
-in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S n0) 
-\Rightarrow (match n0 in nat return (\lambda (_: nat).Prop) with [O 
-\Rightarrow False | (S _) \Rightarrow True])]) | (THead _ _ _) \Rightarrow 
-False])) I (TLRef (S O)) H46) in (False_ind P H47)))))) H43))))) 
-(pc3_gen_abst (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind 
-Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) x0 x5 x1 H7))))))) 
-H34)))))))) H30)) (ty3_gen_lref g (CHead (CHead (CSort O) (Bind Abst) (TSort 
-O)) (Bind Abst) (TSort O)) x4 O H22))))))) H24)))))))) H17))))) H14)))))))) 
-H10)) (ty3_gen_lref g (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
-(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) x6 (S (S O)) H8))))))) 
-(ty3_gen_bind g Abst (CHead (CHead (CHead (CSort O) (Bind Abst) (TSort O)) 
-(Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) (TSort O) 
-(THead (Bind Abst) x0 x1) H1)))))))) H3)) (ty3_gen_lref g (CHead (CHead 
-(CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) 
-(TLRef O)) x0 O H2))))))) (ty3_gen_appl g (CHead (CHead (CHead (CSort O) 
-(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef 
-O) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)) u H))))).
-(* COMMENTS
-Initial nodes: 9973
-END *)
+(TLRef (S (S O))) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow 
+False | (TLRef n) \Rightarrow (match n with [O \Rightarrow False | (S n0) 
+\Rightarrow (match n0 with [O \Rightarrow False | (S _) \Rightarrow True])]) 
+| (THead _ _ _) \Rightarrow False])) I (TLRef (S O)) H46) in (False_ind P 
+H47)))))) H43))))) (pc3_gen_abst (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) x0 
+x5 x1 H7))))))) H34)))))))) H30)) (ty3_gen_lref g (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) x4 O H22))))))) H24)))))))) 
+H17))))) H14)))))))) H10)) (ty3_gen_lref g (CHead (CHead (CHead (CSort O) 
+(Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) x6 (S (S 
+O)) H8))))))) (ty3_gen_bind g Abst (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) 
+(TSort O) (THead (Bind Abst) x0 x1) H1)))))))) H3)) (ty3_gen_lref g (CHead 
+(CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind 
+Abst) (TLRef O)) x0 O H2))))))) (ty3_gen_appl g (CHead (CHead (CHead (CSort 
+O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) 
+(TLRef O) (THead (Bind Abst) (TLRef (S (S O))) (TSort O)) u H))))).