X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fsty0%2Ffwd.ma;h=0d05ca147abaab635f5ebb329553b0d20ad08781;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=134ec3c107c627ab935d27abbb28df6fd8076574;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
index 134ec3c10..0d05ca147 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
@@ -14,9 +14,36 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/sty0/defs.ma".
+include "basic_1/sty0/defs.ma".
 
-theorem sty0_gen_sort:
+implied rec lemma sty0_ind (g: G) (P: (C \to (T \to (T \to Prop)))) (f: 
+(\forall (c: C).(\forall (n: nat).(P c (TSort n) (TSort (next g n)))))) (f0: 
+(\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c 
+(CHead d (Bind Abbr) v)) \to (\forall (w: T).((sty0 g d v w) \to ((P d v w) 
+\to (P c (TLRef i) (lift (S i) O w))))))))))) (f1: (\forall (c: C).(\forall 
+(d: C).(\forall (v: T).(\forall (i: nat).((getl i c (CHead d (Bind Abst) v)) 
+\to (\forall (w: T).((sty0 g d v w) \to ((P d v w) \to (P c (TLRef i) (lift 
+(S i) O v))))))))))) (f2: (\forall (b: B).(\forall (c: C).(\forall (v: 
+T).(\forall (t1: T).(\forall (t2: T).((sty0 g (CHead c (Bind b) v) t1 t2) \to 
+((P (CHead c (Bind b) v) t1 t2) \to (P c (THead (Bind b) v t1) (THead (Bind 
+b) v t2)))))))))) (f3: (\forall (c: C).(\forall (v: T).(\forall (t1: 
+T).(\forall (t2: T).((sty0 g c t1 t2) \to ((P c t1 t2) \to (P c (THead (Flat 
+Appl) v t1) (THead (Flat Appl) v t2))))))))) (f4: (\forall (c: C).(\forall 
+(v1: T).(\forall (v2: T).((sty0 g c v1 v2) \to ((P c v1 v2) \to (\forall (t1: 
+T).(\forall (t2: T).((sty0 g c t1 t2) \to ((P c t1 t2) \to (P c (THead (Flat 
+Cast) v1 t1) (THead (Flat Cast) v2 t2)))))))))))) (c: C) (t: T) (t0: T) (s0: 
+sty0 g c t t0) on s0: P c t t0 \def match s0 with [(sty0_sort c0 n) 
+\Rightarrow (f c0 n) | (sty0_abbr c0 d v i g0 w s1) \Rightarrow (f0 c0 d v i 
+g0 w s1 ((sty0_ind g P f f0 f1 f2 f3 f4) d v w s1)) | (sty0_abst c0 d v i g0 
+w s1) \Rightarrow (f1 c0 d v i g0 w s1 ((sty0_ind g P f f0 f1 f2 f3 f4) d v w 
+s1)) | (sty0_bind b c0 v t1 t2 s1) \Rightarrow (f2 b c0 v t1 t2 s1 ((sty0_ind 
+g P f f0 f1 f2 f3 f4) (CHead c0 (Bind b) v) t1 t2 s1)) | (sty0_appl c0 v t1 
+t2 s1) \Rightarrow (f3 c0 v t1 t2 s1 ((sty0_ind g P f f0 f1 f2 f3 f4) c0 t1 
+t2 s1)) | (sty0_cast c0 v1 v2 s1 t1 t2 s2) \Rightarrow (f4 c0 v1 v2 s1 
+((sty0_ind g P f f0 f1 f2 f3 f4) c0 v1 v2 s1) t1 t2 s2 ((sty0_ind g P f f0 f1 
+f2 f3 f4) c0 t1 t2 s2))].
+
+lemma sty0_gen_sort:
  \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((sty0 g c 
 (TSort n) x) \to (eq T x (TSort (next g n)))))))
 \def
@@ -26,55 +53,49 @@ t x)) (\lambda (_: T).(eq T x (TSort (next g n)))) (\lambda (y: T).(\lambda
 (H0: (sty0 g c y x)).(sty0_ind g (\lambda (_: C).(\lambda (t: T).(\lambda 
 (t0: T).((eq T t (TSort n)) \to (eq T t0 (TSort (next g n))))))) (\lambda (_: 
 C).(\lambda (n0: nat).(\lambda (H1: (eq T (TSort n0) (TSort n))).(let H2 \def 
-(f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with 
-[(TSort n1) \Rightarrow n1 | (TLRef _) \Rightarrow n0 | (THead _ _ _) 
-\Rightarrow n0])) (TSort n0) (TSort n) H1) in (eq_ind_r nat n (\lambda (n1: 
-nat).(eq T (TSort (next g n1)) (TSort (next g n)))) (refl_equal T (TSort 
-(next g n))) n0 H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (v: 
-T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr) 
-v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T v 
-(TSort n)) \to (eq T w (TSort (next g n)))))).(\lambda (H4: (eq T (TLRef i) 
-(TSort n))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T 
-return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
-\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n) H4) in 
-(False_ind (eq T (lift (S i) O w) (TSort (next g n))) H5))))))))))) (\lambda 
-(c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl 
-i c0 (CHead d (Bind Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v 
+(f_equal T nat (\lambda (e: T).(match e with [(TSort n1) \Rightarrow n1 | 
+(TLRef _) \Rightarrow n0 | (THead _ _ _) \Rightarrow n0])) (TSort n0) (TSort 
+n) H1) in (eq_ind_r nat n (\lambda (n1: nat).(eq T (TSort (next g n1)) (TSort 
+(next g n)))) (refl_equal T (TSort (next g n))) n0 H2))))) (\lambda (c0: 
+C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 
+(CHead d (Bind Abbr) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v 
 w)).(\lambda (_: (((eq T v (TSort n)) \to (eq T w (TSort (next g 
 n)))))).(\lambda (H4: (eq T (TLRef i) (TSort n))).(let H5 \def (eq_ind T 
-(TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with 
-[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) 
-\Rightarrow False])) I (TSort n) H4) in (False_ind (eq T (lift (S i) O v) 
-(TSort (next g n))) H5))))))))))) (\lambda (b: B).(\lambda (c0: C).(\lambda 
-(v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (sty0 g (CHead c0 (Bind 
-b) v) t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2 (TSort (next g 
-n)))))).(\lambda (H3: (eq T (THead (Bind b) v t1) (TSort n))).(let H4 \def 
-(eq_ind T (THead (Bind b) v t1) (\lambda (ee: T).(match ee in T return 
-(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
+(TLRef i) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | 
+(TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n) 
+H4) in (False_ind (eq T (lift (S i) O w) (TSort (next g n))) H5))))))))))) 
+(\lambda (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda 
+(_: (getl i c0 (CHead d (Bind Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g 
+d v w)).(\lambda (_: (((eq T v (TSort n)) \to (eq T w (TSort (next g 
+n)))))).(\lambda (H4: (eq T (TLRef i) (TSort n))).(let H5 \def (eq_ind T 
+(TLRef i) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | 
+(TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (TSort n) 
+H4) in (False_ind (eq T (lift (S i) O v) (TSort (next g n))) H5))))))))))) 
+(\lambda (b: B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t1: T).(\lambda 
+(t2: T).(\lambda (_: (sty0 g (CHead c0 (Bind b) v) t1 t2)).(\lambda (_: (((eq 
+T t1 (TSort n)) \to (eq T t2 (TSort (next g n)))))).(\lambda (H3: (eq T 
+(THead (Bind b) v t1) (TSort n))).(let H4 \def (eq_ind T (THead (Bind b) v 
+t1) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) 
 \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H3) in 
 (False_ind (eq T (THead (Bind b) v t2) (TSort (next g n))) H4)))))))))) 
 (\lambda (c0: C).(\lambda (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
 (_: (sty0 g c0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2 (TSort 
 (next g n)))))).(\lambda (H3: (eq T (THead (Flat Appl) v t1) (TSort n))).(let 
-H4 \def (eq_ind T (THead (Flat Appl) v t1) (\lambda (ee: T).(match ee in T 
-return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
-\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H3) in 
-(False_ind (eq T (THead (Flat Appl) v t2) (TSort (next g n))) H4))))))))) 
-(\lambda (c0: C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (sty0 g c0 v1 
-v2)).(\lambda (_: (((eq T v1 (TSort n)) \to (eq T v2 (TSort (next g 
-n)))))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t1 
-t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq T t2 (TSort (next g 
-n)))))).(\lambda (H5: (eq T (THead (Flat Cast) v1 t1) (TSort n))).(let H6 
-\def (eq_ind T (THead (Flat Cast) v1 t1) (\lambda (ee: T).(match ee in T 
-return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
-\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n) H5) in 
-(False_ind (eq T (THead (Flat Cast) v2 t2) (TSort (next g n))) H6)))))))))))) 
-c y x H0))) H))))).
-(* COMMENTS
-Initial nodes: 869
-END *)
+H4 \def (eq_ind T (THead (Flat Appl) v t1) (\lambda (ee: T).(match ee with 
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) 
+\Rightarrow True])) I (TSort n) H3) in (False_ind (eq T (THead (Flat Appl) v 
+t2) (TSort (next g n))) H4))))))))) (\lambda (c0: C).(\lambda (v1: 
+T).(\lambda (v2: T).(\lambda (_: (sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1 
+(TSort n)) \to (eq T v2 (TSort (next g n)))))).(\lambda (t1: T).(\lambda (t2: 
+T).(\lambda (_: (sty0 g c0 t1 t2)).(\lambda (_: (((eq T t1 (TSort n)) \to (eq 
+T t2 (TSort (next g n)))))).(\lambda (H5: (eq T (THead (Flat Cast) v1 t1) 
+(TSort n))).(let H6 \def (eq_ind T (THead (Flat Cast) v1 t1) (\lambda (ee: 
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
+| (THead _ _ _) \Rightarrow True])) I (TSort n) H5) in (False_ind (eq T 
+(THead (Flat Cast) v2 t2) (TSort (next g n))) H6)))))))))))) c y x H0))) 
+H))))).
 
-theorem sty0_gen_lref:
+lemma sty0_gen_lref:
  \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((sty0 g c 
 (TLRef n) x) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda 
 (_: T).(getl n c (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: 
@@ -103,65 +124,63 @@ n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda
 (t1: T).(sty0 g e u t1)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: 
 T).(eq T t0 (lift (S n) O u))))))))))) (\lambda (c0: C).(\lambda (n0: 
 nat).(\lambda (H1: (eq T (TSort n0) (TLRef n))).(let H2 \def (eq_ind T (TSort 
-n0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
-_) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow 
-False])) I (TLRef n) H1) in (False_ind (or (ex3_3 C T T (\lambda (e: 
-C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) 
-(\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda 
-(_: C).(\lambda (_: T).(\lambda (t: T).(eq T (TSort (next g n0)) (lift (S n) 
-O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl 
-n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: 
-T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T 
-(TSort (next g n0)) (lift (S n) O u))))))) H2))))) (\lambda (c0: C).(\lambda 
-(d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H1: (getl i c0 (CHead d 
-(Bind Abbr) v))).(\lambda (w: T).(\lambda (H2: (sty0 g d v w)).(\lambda (_: 
-(((eq T v (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: 
-T).(\lambda (_: T).(getl n d (CHead e (Bind Abbr) u))))) (\lambda (e: 
-C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda 
-(_: T).(\lambda (t: T).(eq T w (lift (S n) O t)))))) (ex3_3 C T T (\lambda 
-(e: C).(\lambda (u: T).(\lambda (_: T).(getl n d (CHead e (Bind Abst) u))))) 
-(\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda 
-(_: C).(\lambda (u: T).(\lambda (_: T).(eq T w (lift (S n) O 
-u)))))))))).(\lambda (H4: (eq T (TLRef i) (TLRef n))).(let H5 \def (f_equal T 
-nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _) 
-\Rightarrow i | (TLRef n0) \Rightarrow n0 | (THead _ _ _) \Rightarrow i])) 
-(TLRef i) (TLRef n) H4) in (let H6 \def (eq_ind nat i (\lambda (n0: 
-nat).(getl n0 c0 (CHead d (Bind Abbr) v))) H1 n H5) in (eq_ind_r nat n 
-(\lambda (n0: nat).(or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda 
-(_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: 
+n0) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow True | (TLRef _) 
+\Rightarrow False | (THead _ _ _) \Rightarrow False])) I (TLRef n) H1) in 
+(False_ind (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: 
+T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: 
 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda 
-(t: T).(eq T (lift (S n0) O w) (lift (S n) O t)))))) (ex3_3 C T T (\lambda 
+(t: T).(eq T (TSort (next g n0)) (lift (S n) O t)))))) (ex3_3 C T T (\lambda 
 (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) 
 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda 
-(_: C).(\lambda (u: T).(\lambda (_: T).(eq T (lift (S n0) O w) (lift (S n) O 
-u)))))))) (or_introl (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda 
-(_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: 
-T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda 
-(t: T).(eq T (lift (S n) O w) (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: 
-C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) 
-(\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda 
-(_: C).(\lambda (u: T).(\lambda (_: T).(eq T (lift (S n) O w) (lift (S n) O 
-u)))))) (ex3_3_intro C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: 
-T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: 
-T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda 
-(t: T).(eq T (lift (S n) O w) (lift (S n) O t))))) d v w H6 H2 (refl_equal T 
-(lift (S n) O w)))) i H5)))))))))))) (\lambda (c0: C).(\lambda (d: 
-C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H1: (getl i c0 (CHead d (Bind 
-Abst) v))).(\lambda (w: T).(\lambda (H2: (sty0 g d v w)).(\lambda (_: (((eq T 
-v (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda 
-(_: T).(getl n d (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: 
-T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda 
-(t: T).(eq T w (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda 
-(u: T).(\lambda (_: T).(getl n d (CHead e (Bind Abst) u))))) (\lambda (e: 
-C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda 
-(u: T).(\lambda (_: T).(eq T w (lift (S n) O u)))))))))).(\lambda (H4: (eq T 
-(TLRef i) (TLRef n))).(let H5 \def (f_equal T nat (\lambda (e: T).(match e in 
-T return (\lambda (_: T).nat) with [(TSort _) \Rightarrow i | (TLRef n0) 
-\Rightarrow n0 | (THead _ _ _) \Rightarrow i])) (TLRef i) (TLRef n) H4) in 
-(let H6 \def (eq_ind nat i (\lambda (n0: nat).(getl n0 c0 (CHead d (Bind 
-Abst) v))) H1 n H5) in (eq_ind_r nat n (\lambda (n0: nat).(or (ex3_3 C T T 
+(_: C).(\lambda (u: T).(\lambda (_: T).(eq T (TSort (next g n0)) (lift (S n) 
+O u))))))) H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda 
+(i: nat).(\lambda (H1: (getl i c0 (CHead d (Bind Abbr) v))).(\lambda (w: 
+T).(\lambda (H2: (sty0 g d v w)).(\lambda (_: (((eq T v (TLRef n)) \to (or 
+(ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n d (CHead 
+e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g 
+e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T w (lift (S n) 
+O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl 
+n d (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: 
+T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T w 
+(lift (S n) O u)))))))))).(\lambda (H4: (eq T (TLRef i) (TLRef n))).(let H5 
+\def (f_equal T nat (\lambda (e: T).(match e with [(TSort _) \Rightarrow i | 
+(TLRef n0) \Rightarrow n0 | (THead _ _ _) \Rightarrow i])) (TLRef i) (TLRef 
+n) H4) in (let H6 \def (eq_ind nat i (\lambda (n0: nat).(getl n0 c0 (CHead d 
+(Bind Abbr) v))) H1 n H5) in (eq_ind_r nat n (\lambda (n0: nat).(or (ex3_3 C 
+T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind 
+Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u 
+t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (lift (S n0) O w) 
+(lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda 
+(_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: 
+T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda 
+(_: T).(eq T (lift (S n0) O w) (lift (S n) O u)))))))) (or_introl (ex3_3 C T 
+T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind 
+Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u 
+t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (lift (S n) O w) 
+(lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda 
+(_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: 
+T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda 
+(_: T).(eq T (lift (S n) O w) (lift (S n) O u)))))) (ex3_3_intro C T T 
 (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind 
 Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u 
+t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (lift (S n) O w) 
+(lift (S n) O t))))) d v w H6 H2 (refl_equal T (lift (S n) O w)))) i 
+H5)))))))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: 
+nat).(\lambda (H1: (getl i c0 (CHead d (Bind Abst) v))).(\lambda (w: 
+T).(\lambda (H2: (sty0 g d v w)).(\lambda (_: (((eq T v (TLRef n)) \to (or 
+(ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n d (CHead 
+e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g 
+e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T w (lift (S n) 
+O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl 
+n d (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: 
+T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T w 
+(lift (S n) O u)))))))))).(\lambda (H4: (eq T (TLRef i) (TLRef n))).(let H5 
+\def (f_equal T nat (\lambda (e: T).(match e with [(TSort _) \Rightarrow i | 
+(TLRef n0) \Rightarrow n0 | (THead _ _ _) \Rightarrow i])) (TLRef i) (TLRef 
+n) H4) in (let H6 \def (eq_ind nat i (\lambda (n0: nat).(getl n0 c0 (CHead d 
+(Bind Abst) v))) H1 n H5) in (eq_ind_r nat n (\lambda (n0: nat).(or (ex3_3 C 
+T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind 
+Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u 
 t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (lift (S n0) O v) 
 (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda 
 (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: 
@@ -189,69 +208,65 @@ n (CHead c0 (Bind b) v) (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda
 (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: 
 T).(\lambda (_: T).(eq T t2 (lift (S n) O u)))))))))).(\lambda (H3: (eq T 
 (THead (Bind b) v t1) (TLRef n))).(let H4 \def (eq_ind T (THead (Bind b) v 
-t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort 
-_) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) 
+t1) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H3) in 
+(False_ind (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: 
+T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: 
+T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda 
+(t: T).(eq T (THead (Bind b) v t2) (lift (S n) O t)))))) (ex3_3 C T T 
+(\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind 
+Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u 
+t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T (THead (Bind b) v 
+t2) (lift (S n) O u))))))) H4)))))))))) (\lambda (c0: C).(\lambda (v: 
+T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t1 t2)).(\lambda 
+(_: (((eq T t1 (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: 
+T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: 
+C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda 
+(_: T).(\lambda (t: T).(eq T t2 (lift (S n) O t)))))) (ex3_3 C T T (\lambda 
+(e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) 
+(\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda 
+(_: C).(\lambda (u: T).(\lambda (_: T).(eq T t2 (lift (S n) O 
+u)))))))))).(\lambda (H3: (eq T (THead (Flat Appl) v t1) (TLRef n))).(let H4 
+\def (eq_ind T (THead (Flat Appl) v t1) (\lambda (ee: T).(match ee with 
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) 
 \Rightarrow True])) I (TLRef n) H3) in (False_ind (or (ex3_3 C T T (\lambda 
 (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) 
 (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda 
-(_: C).(\lambda (_: T).(\lambda (t: T).(eq T (THead (Bind b) v t2) (lift (S 
-n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: 
+(_: C).(\lambda (_: T).(\lambda (t: T).(eq T (THead (Flat Appl) v t2) (lift 
+(S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: 
 T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: 
 T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda 
-(_: T).(eq T (THead (Bind b) v t2) (lift (S n) O u))))))) H4)))))))))) 
-(\lambda (c0: C).(\lambda (v: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
-(_: (sty0 g c0 t1 t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (or (ex3_3 C T 
-T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind 
-Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u 
-t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T t2 (lift (S n) O 
-t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n 
-c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: 
-T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T t2 
-(lift (S n) O u)))))))))).(\lambda (H3: (eq T (THead (Flat Appl) v t1) (TLRef 
-n))).(let H4 \def (eq_ind T (THead (Flat Appl) v t1) (\lambda (ee: T).(match 
-ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | 
-(TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) 
-H3) in (False_ind (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda 
-(_: T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: 
-T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda 
-(t: T).(eq T (THead (Flat Appl) v t2) (lift (S n) O t)))))) (ex3_3 C T T 
-(\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind 
-Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u 
-t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T (THead (Flat 
-Appl) v t2) (lift (S n) O u))))))) H4))))))))) (\lambda (c0: C).(\lambda (v1: 
-T).(\lambda (v2: T).(\lambda (_: (sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1 
-(TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: 
-T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: 
-T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda 
-(t: T).(eq T v2 (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda 
-(u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: 
-C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda 
-(u: T).(\lambda (_: T).(eq T v2 (lift (S n) O u)))))))))).(\lambda (t1: 
-T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t1 t2)).(\lambda (_: (((eq T t1 
-(TLRef n)) \to (or (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: 
-T).(getl n c0 (CHead e (Bind Abbr) u))))) (\lambda (e: C).(\lambda (u: 
-T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (_: T).(\lambda 
-(t: T).(eq T t2 (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda 
-(u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: 
-C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda 
-(u: T).(\lambda (_: T).(eq T t2 (lift (S n) O u)))))))))).(\lambda (H5: (eq T 
-(THead (Flat Cast) v1 t1) (TLRef n))).(let H6 \def (eq_ind T (THead (Flat 
-Cast) v1 t1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) 
-with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ 
-_) \Rightarrow True])) I (TLRef n) H5) in (False_ind (or (ex3_3 C T T 
-(\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind 
-Abbr) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u 
-t)))) (\lambda (_: C).(\lambda (_: T).(\lambda (t: T).(eq T (THead (Flat 
-Cast) v2 t2) (lift (S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: 
-T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: 
-C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda 
-(u: T).(\lambda (_: T).(eq T (THead (Flat Cast) v2 t2) (lift (S n) O u))))))) 
-H6)))))))))))) c y x H0))) H))))).
-(* COMMENTS
-Initial nodes: 3231
-END *)
+(_: T).(eq T (THead (Flat Appl) v t2) (lift (S n) O u))))))) H4))))))))) 
+(\lambda (c0: C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (sty0 g c0 v1 
+v2)).(\lambda (_: (((eq T v1 (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: 
+C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) 
+(\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda 
+(_: C).(\lambda (_: T).(\lambda (t: T).(eq T v2 (lift (S n) O t)))))) (ex3_3 
+C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e 
+(Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e 
+u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T v2 (lift (S n) 
+O u)))))))))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t1 
+t2)).(\lambda (_: (((eq T t1 (TLRef n)) \to (or (ex3_3 C T T (\lambda (e: 
+C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) 
+(\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda 
+(_: C).(\lambda (_: T).(\lambda (t: T).(eq T t2 (lift (S n) O t)))))) (ex3_3 
+C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e 
+(Bind Abst) u))))) (\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e 
+u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda (_: T).(eq T t2 (lift (S n) 
+O u)))))))))).(\lambda (H5: (eq T (THead (Flat Cast) v1 t1) (TLRef n))).(let 
+H6 \def (eq_ind T (THead (Flat Cast) v1 t1) (\lambda (ee: T).(match ee with 
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _ _) 
+\Rightarrow True])) I (TLRef n) H5) in (False_ind (or (ex3_3 C T T (\lambda 
+(e: C).(\lambda (u: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u))))) 
+(\lambda (e: C).(\lambda (u: T).(\lambda (t: T).(sty0 g e u t)))) (\lambda 
+(_: C).(\lambda (_: T).(\lambda (t: T).(eq T (THead (Flat Cast) v2 t2) (lift 
+(S n) O t)))))) (ex3_3 C T T (\lambda (e: C).(\lambda (u: T).(\lambda (_: 
+T).(getl n c0 (CHead e (Bind Abst) u))))) (\lambda (e: C).(\lambda (u: 
+T).(\lambda (t: T).(sty0 g e u t)))) (\lambda (_: C).(\lambda (u: T).(\lambda 
+(_: T).(eq T (THead (Flat Cast) v2 t2) (lift (S n) O u))))))) H6)))))))))))) 
+c y x H0))) H))))).
 
-theorem sty0_gen_bind:
+lemma sty0_gen_bind:
  \forall (g: G).(\forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t1: 
 T).(\forall (x: T).((sty0 g c (THead (Bind b) u t1) x) \to (ex2 T (\lambda 
 (t2: T).(sty0 g (CHead c (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T x (THead 
@@ -267,17 +282,16 @@ x)).(insert_eq T (THead (Bind b) u t1) (\lambda (t: T).(sty0 g c t x))
 (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T t0 (THead (Bind b) u 
 t2)))))))) (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T (TSort n) 
 (THead (Bind b) u t1))).(let H2 \def (eq_ind T (TSort n) (\lambda (ee: 
-T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
-True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I 
-(THead (Bind b) u t1) H1) in (False_ind (ex2 T (\lambda (t2: T).(sty0 g 
-(CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T (TSort (next g n)) 
-(THead (Bind b) u t2)))) H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda 
-(v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr) 
-v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T v 
-(THead (Bind b) u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g (CHead d (Bind b) 
-u) t1 t2)) (\lambda (t2: T).(eq T w (THead (Bind b) u t2))))))).(\lambda (H4: 
-(eq T (TLRef i) (THead (Bind b) u t1))).(let H5 \def (eq_ind T (TLRef i) 
-(\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
+T).(match ee with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | 
+(THead _ _ _) \Rightarrow False])) I (THead (Bind b) u t1) H1) in (False_ind 
+(ex2 T (\lambda (t2: T).(sty0 g (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: 
+T).(eq T (TSort (next g n)) (THead (Bind b) u t2)))) H2))))) (\lambda (c0: 
+C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 
+(CHead d (Bind Abbr) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v 
+w)).(\lambda (_: (((eq T v (THead (Bind b) u t1)) \to (ex2 T (\lambda (t2: 
+T).(sty0 g (CHead d (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T w (THead (Bind 
+b) u t2))))))).(\lambda (H4: (eq T (TLRef i) (THead (Bind b) u t1))).(let H5 
+\def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee with [(TSort _) 
 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow 
 False])) I (THead (Bind b) u t1) H4) in (False_ind (ex2 T (\lambda (t2: 
 T).(sty0 g (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T (lift (S i) O 
@@ -287,78 +301,71 @@ Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T
 v (THead (Bind b) u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g (CHead d (Bind 
 b) u) t1 t2)) (\lambda (t2: T).(eq T w (THead (Bind b) u t2))))))).(\lambda 
 (H4: (eq T (TLRef i) (THead (Bind b) u t1))).(let H5 \def (eq_ind T (TLRef i) 
-(\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
-\Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow 
-False])) I (THead (Bind b) u t1) H4) in (False_ind (ex2 T (\lambda (t2: 
-T).(sty0 g (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T (lift (S i) O 
-v) (THead (Bind b) u t2)))) H5))))))))))) (\lambda (b0: B).(\lambda (c0: 
-C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H1: (sty0 g 
-(CHead c0 (Bind b0) v) t0 t2)).(\lambda (H2: (((eq T t0 (THead (Bind b) u 
-t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind 
-b) u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda 
-(H3: (eq T (THead (Bind b0) v t0) (THead (Bind b) u t1))).(let H4 \def 
-(f_equal T B (\lambda (e: T).(match e in T return (\lambda (_: T).B) with 
-[(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 | (THead k _ _) 
-\Rightarrow (match k in K return (\lambda (_: K).B) with [(Bind b1) 
-\Rightarrow b1 | (Flat _) \Rightarrow b0])])) (THead (Bind b0) v t0) (THead 
-(Bind b) u t1) H3) in ((let H5 \def (f_equal T T (\lambda (e: T).(match e in 
-T return (\lambda (_: T).T) with [(TSort _) \Rightarrow v | (TLRef _) 
-\Rightarrow v | (THead _ t _) \Rightarrow t])) (THead (Bind b0) v t0) (THead 
-(Bind b) u t1) H3) in ((let H6 \def (f_equal T T (\lambda (e: T).(match e in 
-T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) 
-\Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead (Bind b0) v t0) (THead 
-(Bind b) u t1) H3) in (\lambda (H7: (eq T v u)).(\lambda (H8: (eq B b0 
-b)).(let H9 \def (eq_ind T t0 (\lambda (t: T).((eq T t (THead (Bind b) u t1)) 
-\to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind b) u) 
-t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3)))))) H2 t1 H6) in 
-(let H10 \def (eq_ind T t0 (\lambda (t: T).(sty0 g (CHead c0 (Bind b0) v) t 
-t2)) H1 t1 H6) in (let H11 \def (eq_ind T v (\lambda (t: T).((eq T t1 (THead 
-(Bind b) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind 
-b0) t) (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u 
-t3)))))) H9 u H7) in (let H12 \def (eq_ind T v (\lambda (t: T).(sty0 g (CHead 
-c0 (Bind b0) t) t1 t2)) H10 u H7) in (eq_ind_r T u (\lambda (t: T).(ex2 T 
+(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Bind b) u t1) 
+H4) in (False_ind (ex2 T (\lambda (t2: T).(sty0 g (CHead c0 (Bind b) u) t1 
+t2)) (\lambda (t2: T).(eq T (lift (S i) O v) (THead (Bind b) u t2)))) 
+H5))))))))))) (\lambda (b0: B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t0: 
+T).(\lambda (t2: T).(\lambda (H1: (sty0 g (CHead c0 (Bind b0) v) t0 
+t2)).(\lambda (H2: (((eq T t0 (THead (Bind b) u t1)) \to (ex2 T (\lambda (t3: 
+T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind b) u) t1 t3)) (\lambda (t3: 
+T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda (H3: (eq T (THead (Bind b0) 
+v t0) (THead (Bind b) u t1))).(let H4 \def (f_equal T B (\lambda (e: 
+T).(match e with [(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 | 
+(THead k _ _) \Rightarrow (match k with [(Bind b1) \Rightarrow b1 | (Flat _) 
+\Rightarrow b0])])) (THead (Bind b0) v t0) (THead (Bind b) u t1) H3) in ((let 
+H5 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow v | 
+(TLRef _) \Rightarrow v | (THead _ t _) \Rightarrow t])) (THead (Bind b0) v 
+t0) (THead (Bind b) u t1) H3) in ((let H6 \def (f_equal T T (\lambda (e: 
+T).(match e with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | 
+(THead _ _ t) \Rightarrow t])) (THead (Bind b0) v t0) (THead (Bind b) u t1) 
+H3) in (\lambda (H7: (eq T v u)).(\lambda (H8: (eq B b0 b)).(let H9 \def 
+(eq_ind T t0 (\lambda (t: T).((eq T t (THead (Bind b) u t1)) \to (ex2 T 
+(\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) v) (Bind b) u) t1 t3)) 
+(\lambda (t3: T).(eq T t2 (THead (Bind b) u t3)))))) H2 t1 H6) in (let H10 
+\def (eq_ind T t0 (\lambda (t: T).(sty0 g (CHead c0 (Bind b0) v) t t2)) H1 t1 
+H6) in (let H11 \def (eq_ind T v (\lambda (t: T).((eq T t1 (THead (Bind b) u 
+t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead (CHead c0 (Bind b0) t) (Bind 
+b) u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3)))))) H9 u H7) 
+in (let H12 \def (eq_ind T v (\lambda (t: T).(sty0 g (CHead c0 (Bind b0) t) 
+t1 t2)) H10 u H7) in (eq_ind_r T u (\lambda (t: T).(ex2 T (\lambda (t3: 
+T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T (THead (Bind 
+b0) t t2) (THead (Bind b) u t3))))) (let H13 \def (eq_ind B b0 (\lambda (b1: 
+B).((eq T t1 (THead (Bind b) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g 
+(CHead (CHead c0 (Bind b1) u) (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T t2 
+(THead (Bind b) u t3)))))) H11 b H8) in (let H14 \def (eq_ind B b0 (\lambda 
+(b1: B).(sty0 g (CHead c0 (Bind b1) u) t1 t2)) H12 b H8) in (eq_ind_r B b 
+(\lambda (b1: B).(ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 
+t3)) (\lambda (t3: T).(eq T (THead (Bind b1) u t2) (THead (Bind b) u t3))))) 
+(ex_intro2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda 
+(t3: T).(eq T (THead (Bind b) u t2) (THead (Bind b) u t3))) t2 H14 
+(refl_equal T (THead (Bind b) u t2))) b0 H8))) v H7)))))))) H5)) H4)))))))))) 
+(\lambda (c0: C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda 
+(_: (sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind b) u t1)) \to 
+(ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda (t3: 
+T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda (H3: (eq T (THead (Flat 
+Appl) v t0) (THead (Bind b) u t1))).(let H4 \def (eq_ind T (THead (Flat Appl) 
+v t0) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef 
+_) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _) 
+\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) u t1) 
+H3) in (False_ind (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 
+t3)) (\lambda (t3: T).(eq T (THead (Flat Appl) v t2) (THead (Bind b) u t3)))) 
+H4))))))))) (\lambda (c0: C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: 
+(sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind b) u t1)) \to (ex2 T 
+(\lambda (t2: T).(sty0 g (CHead c0 (Bind b) u) t1 t2)) (\lambda (t2: T).(eq T 
+v2 (THead (Bind b) u t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: 
+(sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind b) u t1)) \to (ex2 T 
 (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T 
-(THead (Bind b0) t t2) (THead (Bind b) u t3))))) (let H13 \def (eq_ind B b0 
-(\lambda (b1: B).((eq T t1 (THead (Bind b) u t1)) \to (ex2 T (\lambda (t3: 
-T).(sty0 g (CHead (CHead c0 (Bind b1) u) (Bind b) u) t1 t3)) (\lambda (t3: 
-T).(eq T t2 (THead (Bind b) u t3)))))) H11 b H8) in (let H14 \def (eq_ind B 
-b0 (\lambda (b1: B).(sty0 g (CHead c0 (Bind b1) u) t1 t2)) H12 b H8) in 
-(eq_ind_r B b (\lambda (b1: B).(ex2 T (\lambda (t3: T).(sty0 g (CHead c0 
-(Bind b) u) t1 t3)) (\lambda (t3: T).(eq T (THead (Bind b1) u t2) (THead 
-(Bind b) u t3))))) (ex_intro2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) 
-u) t1 t3)) (\lambda (t3: T).(eq T (THead (Bind b) u t2) (THead (Bind b) u 
-t3))) t2 H14 (refl_equal T (THead (Bind b) u t2))) b0 H8))) v H7)))))))) H5)) 
-H4)))))))))) (\lambda (c0: C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2: 
-T).(\lambda (_: (sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind b) u 
-t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) 
-(\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda (H3: (eq T 
-(THead (Flat Appl) v t0) (THead (Bind b) u t1))).(let H4 \def (eq_ind T 
-(THead (Flat Appl) v t0) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
-(THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
-[(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind 
-b) u t1) H3) in (False_ind (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) 
-u) t1 t3)) (\lambda (t3: T).(eq T (THead (Flat Appl) v t2) (THead (Bind b) u 
-t3)))) H4))))))))) (\lambda (c0: C).(\lambda (v1: T).(\lambda (v2: 
-T).(\lambda (_: (sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind b) u 
-t1)) \to (ex2 T (\lambda (t2: T).(sty0 g (CHead c0 (Bind b) u) t1 t2)) 
-(\lambda (t2: T).(eq T v2 (THead (Bind b) u t2))))))).(\lambda (t0: 
-T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0 
-(THead (Bind b) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) 
-u) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Bind b) u t3))))))).(\lambda 
-(H5: (eq T (THead (Flat Cast) v1 t0) (THead (Bind b) u t1))).(let H6 \def 
-(eq_ind T (THead (Flat Cast) v1 t0) (\lambda (ee: T).(match ee in T return 
-(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
-\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda 
-(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
-True])])) I (THead (Bind b) u t1) H5) in (False_ind (ex2 T (\lambda (t3: 
-T).(sty0 g (CHead c0 (Bind b) u) t1 t3)) (\lambda (t3: T).(eq T (THead (Flat 
-Cast) v2 t2) (THead (Bind b) u t3)))) H6)))))))))))) c y x H0))) H))))))).
-(* COMMENTS
-Initial nodes: 1975
-END *)
+t2 (THead (Bind b) u t3))))))).(\lambda (H5: (eq T (THead (Flat Cast) v1 t0) 
+(THead (Bind b) u t1))).(let H6 \def (eq_ind T (THead (Flat Cast) v1 t0) 
+(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _) 
+\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) u t1) 
+H5) in (False_ind (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind b) u) t1 
+t3)) (\lambda (t3: T).(eq T (THead (Flat Cast) v2 t2) (THead (Bind b) u 
+t3)))) H6)))))))))))) c y x H0))) H))))))).
 
-theorem sty0_gen_appl:
+lemma sty0_gen_appl:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (x: 
 T).((sty0 g c (THead (Flat Appl) u t1) x) \to (ex2 T (\lambda (t2: T).(sty0 g 
 c t1 t2)) (\lambda (t2: T).(eq T x (THead (Flat Appl) u t2)))))))))
@@ -372,82 +379,74 @@ Appl) u t2))))) (\lambda (y: T).(\lambda (H0: (sty0 g c y x)).(sty0_ind g
 u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T 
 t0 (THead (Flat Appl) u t2)))))))) (\lambda (c0: C).(\lambda (n: 
 nat).(\lambda (H1: (eq T (TSort n) (THead (Flat Appl) u t1))).(let H2 \def 
-(eq_ind T (TSort n) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | 
-(THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u t1) H1) in 
-(False_ind (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T 
-(TSort (next g n)) (THead (Flat Appl) u t2)))) H2))))) (\lambda (c0: 
-C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 
-(CHead d (Bind Abbr) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v 
-w)).(\lambda (_: (((eq T v (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t2: 
-T).(sty0 g d t1 t2)) (\lambda (t2: T).(eq T w (THead (Flat Appl) u 
-t2))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Appl) u t1))).(let H5 
-\def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
-(THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u t1) H4) in 
-(False_ind (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T 
-(lift (S i) O w) (THead (Flat Appl) u t2)))) H5))))))))))) (\lambda (c0: 
-C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 
-(CHead d (Bind Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v 
-w)).(\lambda (_: (((eq T v (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t2: 
-T).(sty0 g d t1 t2)) (\lambda (t2: T).(eq T w (THead (Flat Appl) u 
-t2))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Appl) u t1))).(let H5 
-\def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
-(THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u t1) H4) in 
-(False_ind (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T 
-(lift (S i) O v) (THead (Flat Appl) u t2)))) H5))))))))))) (\lambda (b: 
-B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2: 
-T).(\lambda (_: (sty0 g (CHead c0 (Bind b) v) t0 t2)).(\lambda (_: (((eq T t0 
-(THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 (Bind 
-b) v) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Flat Appl) u 
+(eq_ind T (TSort n) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow 
+True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I 
+(THead (Flat Appl) u t1) H1) in (False_ind (ex2 T (\lambda (t2: T).(sty0 g c0 
+t1 t2)) (\lambda (t2: T).(eq T (TSort (next g n)) (THead (Flat Appl) u t2)))) 
+H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: 
+nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr) v))).(\lambda (w: 
+T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T v (THead (Flat Appl) u 
+t1)) \to (ex2 T (\lambda (t2: T).(sty0 g d t1 t2)) (\lambda (t2: T).(eq T w 
+(THead (Flat Appl) u t2))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat 
+Appl) u t1))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee 
+with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ 
+_) \Rightarrow False])) I (THead (Flat Appl) u t1) H4) in (False_ind (ex2 T 
+(\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T (lift (S i) O w) 
+(THead (Flat Appl) u t2)))) H5))))))))))) (\lambda (c0: C).(\lambda (d: 
+C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind 
+Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T 
+v (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g d t1 t2)) 
+(\lambda (t2: T).(eq T w (THead (Flat Appl) u t2))))))).(\lambda (H4: (eq T 
+(TLRef i) (THead (Flat Appl) u t1))).(let H5 \def (eq_ind T (TLRef i) 
+(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) u 
+t1) H4) in (False_ind (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda 
+(t2: T).(eq T (lift (S i) O v) (THead (Flat Appl) u t2)))) H5))))))))))) 
+(\lambda (b: B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t0: T).(\lambda 
+(t2: T).(\lambda (_: (sty0 g (CHead c0 (Bind b) v) t0 t2)).(\lambda (_: (((eq 
+T t0 (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g (CHead c0 
+(Bind b) v) t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Flat Appl) u 
 t3))))))).(\lambda (H3: (eq T (THead (Bind b) v t0) (THead (Flat Appl) u 
 t1))).(let H4 \def (eq_ind T (THead (Bind b) v t0) (\lambda (ee: T).(match ee 
-in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef 
-_) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return 
-(\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow 
-False])])) I (THead (Flat Appl) u t1) H3) in (False_ind (ex2 T (\lambda (t3: 
-T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T (THead (Bind b) v t2) (THead 
-(Flat Appl) u t3)))) H4)))))))))) (\lambda (c0: C).(\lambda (v: T).(\lambda 
-(t0: T).(\lambda (t2: T).(\lambda (H1: (sty0 g c0 t0 t2)).(\lambda (H2: (((eq 
-T t0 (THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) 
-(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u t3))))))).(\lambda (H3: (eq T 
-(THead (Flat Appl) v t0) (THead (Flat Appl) u t1))).(let H4 \def (f_equal T T 
-(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
+with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ 
+_) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat _) 
+\Rightarrow False])])) I (THead (Flat Appl) u t1) H3) in (False_ind (ex2 T 
+(\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T (THead (Bind b) v 
+t2) (THead (Flat Appl) u t3)))) H4)))))))))) (\lambda (c0: C).(\lambda (v: 
+T).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H1: (sty0 g c0 t0 
+t2)).(\lambda (H2: (((eq T t0 (THead (Flat Appl) u t1)) \to (ex2 T (\lambda 
+(t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Flat Appl) u 
+t3))))))).(\lambda (H3: (eq T (THead (Flat Appl) v t0) (THead (Flat Appl) u 
+t1))).(let H4 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
 \Rightarrow v | (TLRef _) \Rightarrow v | (THead _ t _) \Rightarrow t])) 
 (THead (Flat Appl) v t0) (THead (Flat Appl) u t1) H3) in ((let H5 \def 
-(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with 
-[(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) 
-\Rightarrow t])) (THead (Flat Appl) v t0) (THead (Flat Appl) u t1) H3) in 
-(\lambda (H6: (eq T v u)).(let H7 \def (eq_ind T t0 (\lambda (t: T).((eq T t 
-(THead (Flat Appl) u t1)) \to (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) 
-(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u t3)))))) H2 t1 H5) in (let H8 
-\def (eq_ind T t0 (\lambda (t: T).(sty0 g c0 t t2)) H1 t1 H5) in (eq_ind_r T 
-u (\lambda (t: T).(ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: 
-T).(eq T (THead (Flat Appl) t t2) (THead (Flat Appl) u t3))))) (ex_intro2 T 
-(\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T (THead (Flat Appl) 
-u t2) (THead (Flat Appl) u t3))) t2 H8 (refl_equal T (THead (Flat Appl) u 
-t2))) v H6))))) H4))))))))) (\lambda (c0: C).(\lambda (v1: T).(\lambda (v2: 
-T).(\lambda (_: (sty0 g c0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Flat Appl) 
-u t1)) \to (ex2 T (\lambda (t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T 
-v2 (THead (Flat Appl) u t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda 
-(_: (sty0 g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Flat Appl) u t1)) \to 
-(ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T t2 (THead 
-(Flat Appl) u t3))))))).(\lambda (H5: (eq T (THead (Flat Cast) v1 t0) (THead 
-(Flat Appl) u t1))).(let H6 \def (eq_ind T (THead (Flat Cast) v1 t0) (\lambda 
-(ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
-\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
-(match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | 
-(Flat f) \Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl 
-\Rightarrow False | Cast \Rightarrow True])])])) I (THead (Flat Appl) u t1) 
-H5) in (False_ind (ex2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: 
-T).(eq T (THead (Flat Cast) v2 t2) (THead (Flat Appl) u t3)))) H6)))))))))))) 
-c y x H0))) H)))))).
-(* COMMENTS
-Initial nodes: 1489
-END *)
+(f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 | (TLRef 
+_) \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead (Flat Appl) v t0) 
+(THead (Flat Appl) u t1) H3) in (\lambda (H6: (eq T v u)).(let H7 \def 
+(eq_ind T t0 (\lambda (t: T).((eq T t (THead (Flat Appl) u t1)) \to (ex2 T 
+(\lambda (t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Flat 
+Appl) u t3)))))) H2 t1 H5) in (let H8 \def (eq_ind T t0 (\lambda (t: T).(sty0 
+g c0 t t2)) H1 t1 H5) in (eq_ind_r T u (\lambda (t: T).(ex2 T (\lambda (t3: 
+T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T (THead (Flat Appl) t t2) (THead 
+(Flat Appl) u t3))))) (ex_intro2 T (\lambda (t3: T).(sty0 g c0 t1 t3)) 
+(\lambda (t3: T).(eq T (THead (Flat Appl) u t2) (THead (Flat Appl) u t3))) t2 
+H8 (refl_equal T (THead (Flat Appl) u t2))) v H6))))) H4))))))))) (\lambda 
+(c0: C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (sty0 g c0 v1 
+v2)).(\lambda (_: (((eq T v1 (THead (Flat Appl) u t1)) \to (ex2 T (\lambda 
+(t2: T).(sty0 g c0 t1 t2)) (\lambda (t2: T).(eq T v2 (THead (Flat Appl) u 
+t2))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t0 
+t2)).(\lambda (_: (((eq T t0 (THead (Flat Appl) u t1)) \to (ex2 T (\lambda 
+(t3: T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T t2 (THead (Flat Appl) u 
+t3))))))).(\lambda (H5: (eq T (THead (Flat Cast) v1 t0) (THead (Flat Appl) u 
+t1))).(let H6 \def (eq_ind T (THead (Flat Cast) v1 t0) (\lambda (ee: 
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False 
+| (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat 
+f) \Rightarrow (match f with [Appl \Rightarrow False | Cast \Rightarrow 
+True])])])) I (THead (Flat Appl) u t1) H5) in (False_ind (ex2 T (\lambda (t3: 
+T).(sty0 g c0 t1 t3)) (\lambda (t3: T).(eq T (THead (Flat Cast) v2 t2) (THead 
+(Flat Appl) u t3)))) H6)))))))))))) c y x H0))) H)))))).
 
-theorem sty0_gen_cast:
+lemma sty0_gen_cast:
  \forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (t1: T).(\forall 
 (x: T).((sty0 g c (THead (Flat Cast) v1 t1) x) \to (ex3_2 T T (\lambda (v2: 
 T).(\lambda (_: T).(sty0 g c v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 
@@ -465,98 +464,90 @@ T t (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v2: T).(\lambda (_:
 T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2))) 
 (\lambda (v2: T).(\lambda (t2: T).(eq T t0 (THead (Flat Cast) v2 t2))))))))) 
 (\lambda (c0: C).(\lambda (n: nat).(\lambda (H1: (eq T (TSort n) (THead (Flat 
-Cast) v1 t1))).(let H2 \def (eq_ind T (TSort n) (\lambda (ee: T).(match ee in 
-T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) 
-\Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Flat Cast) 
-v1 t1) H1) in (False_ind (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g 
-c0 v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2))) (\lambda 
-(v2: T).(\lambda (t2: T).(eq T (TSort (next g n)) (THead (Flat Cast) v2 
-t2))))) H2))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: 
-nat).(\lambda (_: (getl i c0 (CHead d (Bind Abbr) v))).(\lambda (w: 
-T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T v (THead (Flat Cast) v1 
-t1)) \to (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g d v1 v2))) 
-(\lambda (_: T).(\lambda (t2: T).(sty0 g d t1 t2))) (\lambda (v2: T).(\lambda 
-(t2: T).(eq T w (THead (Flat Cast) v2 t2)))))))).(\lambda (H4: (eq T (TLRef 
-i) (THead (Flat Cast) v1 t1))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: 
-T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
-False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I 
-(THead (Flat Cast) v1 t1) H4) in (False_ind (ex3_2 T T (\lambda (v2: 
-T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 
-g c0 t1 t2))) (\lambda (v2: T).(\lambda (t2: T).(eq T (lift (S i) O w) (THead 
-(Flat Cast) v2 t2))))) H5))))))))))) (\lambda (c0: C).(\lambda (d: 
-C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d (Bind 
-Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: (((eq T 
-v (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v2: T).(\lambda (_: 
-T).(sty0 g d v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 g d t1 t2))) 
+Cast) v1 t1))).(let H2 \def (eq_ind T (TSort n) (\lambda (ee: T).(match ee 
+with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ 
+_) \Rightarrow False])) I (THead (Flat Cast) v1 t1) H1) in (False_ind (ex3_2 
+T T (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: 
+T).(\lambda (t2: T).(sty0 g c0 t1 t2))) (\lambda (v2: T).(\lambda (t2: T).(eq 
+T (TSort (next g n)) (THead (Flat Cast) v2 t2))))) H2))))) (\lambda (c0: 
+C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 
+(CHead d (Bind Abbr) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v 
+w)).(\lambda (_: (((eq T v (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda 
+(v2: T).(\lambda (_: T).(sty0 g d v1 v2))) (\lambda (_: T).(\lambda (t2: 
+T).(sty0 g d t1 t2))) (\lambda (v2: T).(\lambda (t2: T).(eq T w (THead (Flat 
+Cast) v2 t2)))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Cast) v1 
+t1))).(let H5 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee with 
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) 
+\Rightarrow False])) I (THead (Flat Cast) v1 t1) H4) in (False_ind (ex3_2 T T 
+(\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda 
+(t2: T).(sty0 g c0 t1 t2))) (\lambda (v2: T).(\lambda (t2: T).(eq T (lift (S 
+i) O w) (THead (Flat Cast) v2 t2))))) H5))))))))))) (\lambda (c0: C).(\lambda 
+(d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (_: (getl i c0 (CHead d 
+(Bind Abst) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (_: 
+(((eq T v (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v2: T).(\lambda 
+(_: T).(sty0 g d v1 v2))) (\lambda (_: T).(\lambda (t2: T).(sty0 g d t1 t2))) 
 (\lambda (v2: T).(\lambda (t2: T).(eq T w (THead (Flat Cast) v2 
 t2)))))))).(\lambda (H4: (eq T (TLRef i) (THead (Flat Cast) v1 t1))).(let H5 
-\def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: 
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
-(THead _ _ _) \Rightarrow False])) I (THead (Flat Cast) v1 t1) H4) in 
-(False_ind (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) 
-(\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2))) (\lambda (v2: 
-T).(\lambda (t2: T).(eq T (lift (S i) O v) (THead (Flat Cast) v2 t2))))) 
-H5))))))))))) (\lambda (b: B).(\lambda (c0: C).(\lambda (v: T).(\lambda (t0: 
-T).(\lambda (t2: T).(\lambda (_: (sty0 g (CHead c0 (Bind b) v) t0 
-t2)).(\lambda (_: (((eq T t0 (THead (Flat Cast) v1 t1)) \to (ex3_2 T T 
-(\lambda (v2: T).(\lambda (_: T).(sty0 g (CHead c0 (Bind b) v) v1 v2))) 
-(\lambda (_: T).(\lambda (t3: T).(sty0 g (CHead c0 (Bind b) v) t1 t3))) 
-(\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) v2 
+\def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee with [(TSort _) 
+\Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow 
+False])) I (THead (Flat Cast) v1 t1) H4) in (False_ind (ex3_2 T T (\lambda 
+(v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda (t2: 
+T).(sty0 g c0 t1 t2))) (\lambda (v2: T).(\lambda (t2: T).(eq T (lift (S i) O 
+v) (THead (Flat Cast) v2 t2))))) H5))))))))))) (\lambda (b: B).(\lambda (c0: 
+C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (sty0 g 
+(CHead c0 (Bind b) v) t0 t2)).(\lambda (_: (((eq T t0 (THead (Flat Cast) v1 
+t1)) \to (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g (CHead c0 (Bind 
+b) v) v1 v2))) (\lambda (_: T).(\lambda (t3: T).(sty0 g (CHead c0 (Bind b) v) 
+t1 t3))) (\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) v2 
 t3)))))))).(\lambda (H3: (eq T (THead (Bind b) v t0) (THead (Flat Cast) v1 
 t1))).(let H4 \def (eq_ind T (THead (Bind b) v t0) (\lambda (ee: T).(match ee 
-in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef 
-_) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return 
-(\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow 
-False])])) I (THead (Flat Cast) v1 t1) H3) in (False_ind (ex3_2 T T (\lambda 
-(v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda (t3: 
-T).(sty0 g c0 t1 t3))) (\lambda (v2: T).(\lambda (t3: T).(eq T (THead (Bind 
-b) v t2) (THead (Flat Cast) v2 t3))))) H4)))))))))) (\lambda (c0: C).(\lambda 
-(v: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (sty0 g c0 t0 
-t2)).(\lambda (_: (((eq T t0 (THead (Flat Cast) v1 t1)) \to (ex3_2 T T 
-(\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: T).(\lambda 
-(t3: T).(sty0 g c0 t1 t3))) (\lambda (v2: T).(\lambda (t3: T).(eq T t2 (THead 
-(Flat Cast) v2 t3)))))))).(\lambda (H3: (eq T (THead (Flat Appl) v t0) (THead 
-(Flat Cast) v1 t1))).(let H4 \def (eq_ind T (THead (Flat Appl) v t0) (\lambda 
-(ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _) 
-\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow 
-(match k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | 
-(Flat f) \Rightarrow (match f in F return (\lambda (_: F).Prop) with [Appl 
-\Rightarrow True | Cast \Rightarrow False])])])) I (THead (Flat Cast) v1 t1) 
-H3) in (False_ind (ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 
-v2))) (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3))) (\lambda (v2: 
-T).(\lambda (t3: T).(eq T (THead (Flat Appl) v t2) (THead (Flat Cast) v2 
-t3))))) H4))))))))) (\lambda (c0: C).(\lambda (v0: T).(\lambda (v2: 
-T).(\lambda (H1: (sty0 g c0 v0 v2)).(\lambda (H2: (((eq T v0 (THead (Flat 
-Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3: T).(\lambda (_: T).(sty0 g c0 v1 
-v3))) (\lambda (_: T).(\lambda (t2: T).(sty0 g c0 t1 t2))) (\lambda (v3: 
-T).(\lambda (t2: T).(eq T v2 (THead (Flat Cast) v3 t2)))))))).(\lambda (t0: 
-T).(\lambda (t2: T).(\lambda (H3: (sty0 g c0 t0 t2)).(\lambda (H4: (((eq T t0 
-(THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3: T).(\lambda (_: 
-T).(sty0 g c0 v1 v3))) (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3))) 
-(\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) v3 
-t3)))))))).(\lambda (H5: (eq T (THead (Flat Cast) v0 t0) (THead (Flat Cast) 
-v1 t1))).(let H6 \def (f_equal T T (\lambda (e: T).(match e in T return 
-(\lambda (_: T).T) with [(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0 
-| (THead _ t _) \Rightarrow t])) (THead (Flat Cast) v0 t0) (THead (Flat Cast) 
-v1 t1) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e in T return 
-(\lambda (_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 
-| (THead _ _ t) \Rightarrow t])) (THead (Flat Cast) v0 t0) (THead (Flat Cast) 
-v1 t1) H5) in (\lambda (H8: (eq T v0 v1)).(let H9 \def (eq_ind T t0 (\lambda 
-(t: T).((eq T t (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3: 
-T).(\lambda (_: T).(sty0 g c0 v1 v3))) (\lambda (_: T).(\lambda (t3: T).(sty0 
-g c0 t1 t3))) (\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) 
-v3 t3))))))) H4 t1 H7) in (let H10 \def (eq_ind T t0 (\lambda (t: T).(sty0 g 
-c0 t t2)) H3 t1 H7) in (let H11 \def (eq_ind T v0 (\lambda (t: T).((eq T t 
-(THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3: T).(\lambda (_: 
+with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ 
+_) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat _) 
+\Rightarrow False])])) I (THead (Flat Cast) v1 t1) H3) in (False_ind (ex3_2 T 
+T (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: 
+T).(\lambda (t3: T).(sty0 g c0 t1 t3))) (\lambda (v2: T).(\lambda (t3: T).(eq 
+T (THead (Bind b) v t2) (THead (Flat Cast) v2 t3))))) H4)))))))))) (\lambda 
+(c0: C).(\lambda (v: T).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (sty0 
+g c0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Flat Cast) v1 t1)) \to (ex3_2 T 
+T (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: 
+T).(\lambda (t3: T).(sty0 g c0 t1 t3))) (\lambda (v2: T).(\lambda (t3: T).(eq 
+T t2 (THead (Flat Cast) v2 t3)))))))).(\lambda (H3: (eq T (THead (Flat Appl) 
+v t0) (THead (Flat Cast) v1 t1))).(let H4 \def (eq_ind T (THead (Flat Appl) v 
+t0) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) 
+\Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _) 
+\Rightarrow False | (Flat f) \Rightarrow (match f with [Appl \Rightarrow True 
+| Cast \Rightarrow False])])])) I (THead (Flat Cast) v1 t1) H3) in (False_ind 
+(ex3_2 T T (\lambda (v2: T).(\lambda (_: T).(sty0 g c0 v1 v2))) (\lambda (_: 
+T).(\lambda (t3: T).(sty0 g c0 t1 t3))) (\lambda (v2: T).(\lambda (t3: T).(eq 
+T (THead (Flat Appl) v t2) (THead (Flat Cast) v2 t3))))) H4))))))))) (\lambda 
+(c0: C).(\lambda (v0: T).(\lambda (v2: T).(\lambda (H1: (sty0 g c0 v0 
+v2)).(\lambda (H2: (((eq T v0 (THead (Flat Cast) v1 t1)) \to (ex3_2 T T 
+(\lambda (v3: T).(\lambda (_: T).(sty0 g c0 v1 v3))) (\lambda (_: T).(\lambda 
+(t2: T).(sty0 g c0 t1 t2))) (\lambda (v3: T).(\lambda (t2: T).(eq T v2 (THead 
+(Flat Cast) v3 t2)))))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H3: 
+(sty0 g c0 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Flat Cast) v1 t1)) \to 
+(ex3_2 T T (\lambda (v3: T).(\lambda (_: T).(sty0 g c0 v1 v3))) (\lambda (_: 
+T).(\lambda (t3: T).(sty0 g c0 t1 t3))) (\lambda (v3: T).(\lambda (t3: T).(eq 
+T t2 (THead (Flat Cast) v3 t3)))))))).(\lambda (H5: (eq T (THead (Flat Cast) 
+v0 t0) (THead (Flat Cast) v1 t1))).(let H6 \def (f_equal T T (\lambda (e: 
+T).(match e with [(TSort _) \Rightarrow v0 | (TLRef _) \Rightarrow v0 | 
+(THead _ t _) \Rightarrow t])) (THead (Flat Cast) v0 t0) (THead (Flat Cast) 
+v1 t1) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e with 
+[(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t) 
+\Rightarrow t])) (THead (Flat Cast) v0 t0) (THead (Flat Cast) v1 t1) H5) in 
+(\lambda (H8: (eq T v0 v1)).(let H9 \def (eq_ind T t0 (\lambda (t: T).((eq T 
+t (THead (Flat Cast) v1 t1)) \to (ex3_2 T T (\lambda (v3: T).(\lambda (_: 
 T).(sty0 g c0 v1 v3))) (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3))) 
-(\lambda (v3: T).(\lambda (t3: T).(eq T v2 (THead (Flat Cast) v3 t3))))))) H2 
-v1 H8) in (let H12 \def (eq_ind T v0 (\lambda (t: T).(sty0 g c0 t v2)) H1 v1 
-H8) in (ex3_2_intro T T (\lambda (v3: T).(\lambda (_: T).(sty0 g c0 v1 v3))) 
+(\lambda (v3: T).(\lambda (t3: T).(eq T t2 (THead (Flat Cast) v3 t3))))))) H4 
+t1 H7) in (let H10 \def (eq_ind T t0 (\lambda (t: T).(sty0 g c0 t t2)) H3 t1 
+H7) in (let H11 \def (eq_ind T v0 (\lambda (t: T).((eq T t (THead (Flat Cast) 
+v1 t1)) \to (ex3_2 T T (\lambda (v3: T).(\lambda (_: T).(sty0 g c0 v1 v3))) 
+(\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3))) (\lambda (v3: 
+T).(\lambda (t3: T).(eq T v2 (THead (Flat Cast) v3 t3))))))) H2 v1 H8) in 
+(let H12 \def (eq_ind T v0 (\lambda (t: T).(sty0 g c0 t v2)) H1 v1 H8) in 
+(ex3_2_intro T T (\lambda (v3: T).(\lambda (_: T).(sty0 g c0 v1 v3))) 
 (\lambda (_: T).(\lambda (t3: T).(sty0 g c0 t1 t3))) (\lambda (v3: 
 T).(\lambda (t3: T).(eq T (THead (Flat Cast) v2 t2) (THead (Flat Cast) v3 
 t3)))) v2 t2 H12 H10 (refl_equal T (THead (Flat Cast) v2 t2))))))))) 
 H6)))))))))))) c y x H0))) H)))))).
-(* COMMENTS
-Initial nodes: 1855
-END *)