components: G, next_plus, sty0, sty1

diff --git a/matita/matita/contribs/lambdadelta/basic_1/G/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/G/defs.ma
index 23edf578984153bcc9c9068c4c7baf9b08041dcd..ae81c7857dd23e5cea3ae2b977fa51f4192fbef4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/G/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/G/defs.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/preamble.ma".
+include "basic_1/preamble.ma".
 
-record G : Set \def {
+record G : Type[0] \def {
  next: (nat \to nat);
  next_lt: (\forall (n: nat).(lt n (next n)))
 }.

diff --git a/matita/matita/contribs/lambdadelta/basic_1/next_plus/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/next_plus/defs.ma
index 1ff7ecdff3a47aea1e2cf6e71fe67f73b986a553..63eeacb4167e5ab3ca07c964422d68c771ec2768 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/next_plus/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/next_plus/defs.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/G/defs.ma".
+include "basic_1/G/defs.ma".
 
-definition next_plus:
- G \to (nat \to (nat \to nat))
-\def
- let rec next_plus (g: G) (n: nat) (i: nat) on i: nat \def (match i with [O 
-\Rightarrow n | (S i0) \Rightarrow (next g (next_plus g n i0))]) in next_plus.
+let rec next_plus (g: G) (n: nat) (i: nat) on i: nat \def match i with [O 
+\Rightarrow n | (S i0) \Rightarrow (let TMP_1 \def (next_plus g n i0) in 
+(next g TMP_1))].
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma b/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma
index 258c3a711bacce875591a3b84bc4df205d0f9e68..29d7c60d702e8f45b1ab553bebbfb51a15e95cff 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma
@@ -14,55 +14,76 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/next_plus/defs.ma".
+include "basic_1/next_plus/defs.ma".
 
 theorem next_plus_assoc:
  \forall (g: G).(\forall (n: nat).(\forall (h1: nat).(\forall (h2: nat).(eq 
 nat (next_plus g (next_plus g n h1) h2) (next_plus g n (plus h1 h2))))))
 \def
- \lambda (g: G).(\lambda (n: nat).(\lambda (h1: nat).(nat_ind (\lambda (n0: 
-nat).(\forall (h2: nat).(eq nat (next_plus g (next_plus g n n0) h2) 
-(next_plus g n (plus n0 h2))))) (\lambda (h2: nat).(refl_equal nat (next_plus 
-g n h2))) (\lambda (n0: nat).(\lambda (_: ((\forall (h2: nat).(eq nat 
-(next_plus g (next_plus g n n0) h2) (next_plus g n (plus n0 h2)))))).(\lambda 
-(h2: nat).(nat_ind (\lambda (n1: nat).(eq nat (next_plus g (next g (next_plus 
-g n n0)) n1) (next g (next_plus g n (plus n0 n1))))) (eq_ind nat n0 (\lambda 
-(n1: nat).(eq nat (next g (next_plus g n n0)) (next g (next_plus g n n1)))) 
-(refl_equal nat (next g (next_plus g n n0))) (plus n0 O) (plus_n_O n0)) 
-(\lambda (n1: nat).(\lambda (H0: (eq nat (next_plus g (next g (next_plus g n 
-n0)) n1) (next g (next_plus g n (plus n0 n1))))).(eq_ind nat (S (plus n0 n1)) 
-(\lambda (n2: nat).(eq nat (next g (next_plus g (next g (next_plus g n n0)) 
-n1)) (next g (next_plus g n n2)))) (f_equal nat nat (next g) (next_plus g 
-(next g (next_plus g n n0)) n1) (next g (next_plus g n (plus n0 n1))) H0) 
-(plus n0 (S n1)) (plus_n_Sm n0 n1)))) h2)))) h1))).
-(* COMMENTS
-Initial nodes: 351
-END *)
+ \lambda (g: G).(\lambda (n: nat).(\lambda (h1: nat).(let TMP_5 \def (\lambda 
+(n0: nat).(\forall (h2: nat).(let TMP_1 \def (next_plus g n n0) in (let TMP_2 
+\def (next_plus g TMP_1 h2) in (let TMP_3 \def (plus n0 h2) in (let TMP_4 
+\def (next_plus g n TMP_3) in (eq nat TMP_2 TMP_4))))))) in (let TMP_7 \def 
+(\lambda (h2: nat).(let TMP_6 \def (next_plus g n h2) in (refl_equal nat 
+TMP_6))) in (let TMP_47 \def (\lambda (n0: nat).(\lambda (_: ((\forall (h2: 
+nat).(eq nat (next_plus g (next_plus g n n0) h2) (next_plus g n (plus n0 
+h2)))))).(\lambda (h2: nat).(let TMP_14 \def (\lambda (n1: nat).(let TMP_8 
+\def (next_plus g n n0) in (let TMP_9 \def (next g TMP_8) in (let TMP_10 \def 
+(next_plus g TMP_9 n1) in (let TMP_11 \def (plus n0 n1) in (let TMP_12 \def 
+(next_plus g n TMP_11) in (let TMP_13 \def (next g TMP_12) in (eq nat TMP_10 
+TMP_13)))))))) in (let TMP_19 \def (\lambda (n1: nat).(let TMP_15 \def 
+(next_plus g n n0) in (let TMP_16 \def (next g TMP_15) in (let TMP_17 \def 
+(next_plus g n n1) in (let TMP_18 \def (next g TMP_17) in (eq nat TMP_16 
+TMP_18)))))) in (let TMP_20 \def (next_plus g n n0) in (let TMP_21 \def (next 
+g TMP_20) in (let TMP_22 \def (refl_equal nat TMP_21) in (let TMP_23 \def 
+(plus n0 O) in (let TMP_24 \def (plus_n_O n0) in (let TMP_25 \def (eq_ind nat 
+n0 TMP_19 TMP_22 TMP_23 TMP_24) in (let TMP_46 \def (\lambda (n1: 
+nat).(\lambda (H0: (eq nat (next_plus g (next g (next_plus g n n0)) n1) (next 
+g (next_plus g n (plus n0 n1))))).(let TMP_26 \def (plus n0 n1) in (let 
+TMP_27 \def (S TMP_26) in (let TMP_34 \def (\lambda (n2: nat).(let TMP_28 
+\def (next_plus g n n0) in (let TMP_29 \def (next g TMP_28) in (let TMP_30 
+\def (next_plus g TMP_29 n1) in (let TMP_31 \def (next g TMP_30) in (let 
+TMP_32 \def (next_plus g n n2) in (let TMP_33 \def (next g TMP_32) in (eq nat 
+TMP_31 TMP_33)))))))) in (let TMP_35 \def (next g) in (let TMP_36 \def 
+(next_plus g n n0) in (let TMP_37 \def (next g TMP_36) in (let TMP_38 \def 
+(next_plus g TMP_37 n1) in (let TMP_39 \def (plus n0 n1) in (let TMP_40 \def 
+(next_plus g n TMP_39) in (let TMP_41 \def (next g TMP_40) in (let TMP_42 
+\def (f_equal nat nat TMP_35 TMP_38 TMP_41 H0) in (let TMP_43 \def (S n1) in 
+(let TMP_44 \def (plus n0 TMP_43) in (let TMP_45 \def (plus_n_Sm n0 n1) in 
+(eq_ind nat TMP_27 TMP_34 TMP_42 TMP_44 TMP_45))))))))))))))))) in (nat_ind 
+TMP_14 TMP_25 TMP_46 h2))))))))))))) in (nat_ind TMP_5 TMP_7 TMP_47 h1)))))).
 
 theorem next_plus_next:
  \forall (g: G).(\forall (n: nat).(\forall (h: nat).(eq nat (next_plus g 
 (next g n) h) (next g (next_plus g n h)))))
 \def
- \lambda (g: G).(\lambda (n: nat).(\lambda (h: nat).(eq_ind_r nat (next_plus 
-g n (plus (S O) h)) (\lambda (n0: nat).(eq nat n0 (next g (next_plus g n 
-h)))) (refl_equal nat (next g (next_plus g n h))) (next_plus g (next_plus g n 
-(S O)) h) (next_plus_assoc g n (S O) h)))).
-(* COMMENTS
-Initial nodes: 87
-END *)
+ \lambda (g: G).(\lambda (n: nat).(\lambda (h: nat).(let TMP_1 \def (S O) in 
+(let TMP_2 \def (plus TMP_1 h) in (let TMP_3 \def (next_plus g n TMP_2) in 
+(let TMP_6 \def (\lambda (n0: nat).(let TMP_4 \def (next_plus g n h) in (let 
+TMP_5 \def (next g TMP_4) in (eq nat n0 TMP_5)))) in (let TMP_7 \def 
+(next_plus g n h) in (let TMP_8 \def (next g TMP_7) in (let TMP_9 \def 
+(refl_equal nat TMP_8) in (let TMP_10 \def (S O) in (let TMP_11 \def 
+(next_plus g n TMP_10) in (let TMP_12 \def (next_plus g TMP_11 h) in (let 
+TMP_13 \def (S O) in (let TMP_14 \def (next_plus_assoc g n TMP_13 h) in 
+(eq_ind_r nat TMP_3 TMP_6 TMP_9 TMP_12 TMP_14))))))))))))))).
 
 theorem next_plus_lt:
  \forall (g: G).(\forall (h: nat).(\forall (n: nat).(lt n (next_plus g (next 
 g n) h))))
 \def
- \lambda (g: G).(\lambda (h: nat).(nat_ind (\lambda (n: nat).(\forall (n0: 
-nat).(lt n0 (next_plus g (next g n0) n)))) (\lambda (n: nat).(next_lt g n)) 
-(\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(lt n0 (next_plus g (next 
-g n0) n))))).(\lambda (n0: nat).(eq_ind nat (next_plus g (next g (next g n0)) 
-n) (\lambda (n1: nat).(lt n0 n1)) (lt_trans n0 (next g n0) (next_plus g (next 
-g (next g n0)) n) (next_lt g n0) (H (next g n0))) (next g (next_plus g (next 
-g n0) n)) (next_plus_next g (next g n0) n))))) h)).
-(* COMMENTS
-Initial nodes: 153
-END *)
+ \lambda (g: G).(\lambda (h: nat).(let TMP_3 \def (\lambda (n: nat).(\forall 
+(n0: nat).(let TMP_1 \def (next g n0) in (let TMP_2 \def (next_plus g TMP_1 
+n) in (lt n0 TMP_2))))) in (let TMP_4 \def (\lambda (n: nat).(next_lt g n)) 
+in (let TMP_22 \def (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(lt n0 
+(next_plus g (next g n0) n))))).(\lambda (n0: nat).(let TMP_5 \def (next g 
+n0) in (let TMP_6 \def (next g TMP_5) in (let TMP_7 \def (next_plus g TMP_6 
+n) in (let TMP_8 \def (\lambda (n1: nat).(lt n0 n1)) in (let TMP_9 \def (next 
+g n0) in (let TMP_10 \def (next g n0) in (let TMP_11 \def (next g TMP_10) in 
+(let TMP_12 \def (next_plus g TMP_11 n) in (let TMP_13 \def (next_lt g n0) in 
+(let TMP_14 \def (next g n0) in (let TMP_15 \def (H TMP_14) in (let TMP_16 
+\def (lt_trans n0 TMP_9 TMP_12 TMP_13 TMP_15) in (let TMP_17 \def (next g n0) 
+in (let TMP_18 \def (next_plus g TMP_17 n) in (let TMP_19 \def (next g 
+TMP_18) in (let TMP_20 \def (next g n0) in (let TMP_21 \def (next_plus_next g 
+TMP_20 n) in (eq_ind nat TMP_7 TMP_8 TMP_16 TMP_19 
+TMP_21))))))))))))))))))))) in (nat_ind TMP_3 TMP_4 TMP_22 h))))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty0/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/sty0/defs.ma
index 6468d9dbb2ec3886bbf6b193366dd639ec7132ff..e4e0ca832bdf85cdd41520eb3b462173d741b953 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/sty0/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty0/defs.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/G/defs.ma".
+include "basic_1/G/defs.ma".
 
-include "Basic-1/getl/defs.ma".
+include "basic_1/getl/defs.ma".
 
 inductive sty0 (g: G): C \to (T \to (T \to Prop)) \def
 | sty0_sort: \forall (c: C).(\forall (n: nat).(sty0 g c (TSort n) (TSort 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
index 134ec3c107c627ab935d27abbb28df6fd8076574..5dfa365c1ef49d750ad0c418e8d951814ac987dd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty0/fwd.ma
@@ -14,7 +14,34 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/sty0/defs.ma".
+include "basic_1/sty0/defs.ma".
+
+let rec 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))].
 
 theorem sty0_gen_sort:
  \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((sty0 g c 
@@ -26,53 +53,47 @@ 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:
  \forall (g: G).(\forall (c: C).(\forall (x: T).(\forall (n: nat).((sty0 g c 
@@ -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,67 +208,63 @@ 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:
  \forall (g: G).(\forall (b: B).(\forall (c: C).(\forall (u: T).(\forall (t1: 
@@ -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,76 +301,69 @@ 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:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (x: 
@@ -372,80 +379,72 @@ 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:
  \forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (t1: T).(\forall 
@@ -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 *)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty0/props.ma b/matita/matita/contribs/lambdadelta/basic_1/sty0/props.ma
index 00c9f68185b08fc9d46dea5cfa44eff29c2ffd1e..69849f3f143614367804b734f7fdc01ca611cdd8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/sty0/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty0/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/sty0/defs.ma".
+include "basic_1/sty0/fwd.ma".
 
-include "Basic-1/getl/drop.ma".
+include "basic_1/getl/drop.ma".
 
 theorem sty0_lift:
  \forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((sty0 g e 
@@ -39,72 +39,74 @@ nat).((drop h d0 c0 d) \to (sty0 g c0 (lift h d0 v) (lift h d0
 w)))))))).(\lambda (c0: C).(\lambda (h: nat).(\lambda (d0: nat).(\lambda (H3: 
 (drop h d0 c0 c)).(lt_le_e i d0 (sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 
 (lift (S i) O w))) (\lambda (H4: (lt i d0)).(let H5 \def (drop_getl_trans_le 
-i d0 (le_S_n i d0 (le_S (S i) d0 H4)) c0 c h H3 (CHead d (Bind Abbr) v) H0) 
-in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_: C).(drop i O c0 e0))) 
+i d0 (le_S_n i d0 (le_S_n (S i) (S d0) (le_S (S (S i)) (S d0) (le_n_S (S i) 
+d0 H4)))) c0 c h H3 (CHead d (Bind Abbr) v) H0) in (ex3_2_ind C C (\lambda 
+(e0: C).(\lambda (_: C).(drop i O c0 e0))) (\lambda (e0: C).(\lambda (e1: 
+C).(drop h (minus d0 i) e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1 
+(CHead d (Bind Abbr) v)))) (sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift 
+(S i) O w))) (\lambda (x0: C).(\lambda (x1: C).(\lambda (H6: (drop i O c0 
+x0)).(\lambda (H7: (drop h (minus d0 i) x0 x1)).(\lambda (H8: (clear x1 
+(CHead d (Bind Abbr) v))).(let H9 \def (eq_ind nat (minus d0 i) (\lambda (n: 
+nat).(drop h n x0 x1)) H7 (S (minus d0 (S i))) (minus_x_Sy d0 i H4)) in (let 
+H10 \def (drop_clear_S x1 x0 h (minus d0 (S i)) H9 Abbr d v H8) in (ex2_ind C 
+(\lambda (c1: C).(clear x0 (CHead c1 (Bind Abbr) (lift h (minus d0 (S i)) 
+v)))) (\lambda (c1: C).(drop h (minus d0 (S i)) c1 d)) (sty0 g c0 (lift h d0 
+(TLRef i)) (lift h d0 (lift (S i) O w))) (\lambda (x: C).(\lambda (H11: 
+(clear x0 (CHead x (Bind Abbr) (lift h (minus d0 (S i)) v)))).(\lambda (H12: 
+(drop h (minus d0 (S i)) x d)).(eq_ind_r T (TLRef i) (\lambda (t: T).(sty0 g 
+c0 t (lift h d0 (lift (S i) O w)))) (eq_ind nat (plus (S i) (minus d0 (S i))) 
+(\lambda (n: nat).(sty0 g c0 (TLRef i) (lift h n (lift (S i) O w)))) 
+(eq_ind_r T (lift (S i) O (lift h (minus d0 (S i)) w)) (\lambda (t: T).(sty0 
+g c0 (TLRef i) t)) (eq_ind nat d0 (\lambda (_: nat).(sty0 g c0 (TLRef i) 
+(lift (S i) O (lift h (minus d0 (S i)) w)))) (sty0_abbr g c0 x (lift h (minus 
+d0 (S i)) v) i (getl_intro i c0 (CHead x (Bind Abbr) (lift h (minus d0 (S i)) 
+v)) x0 H6 H11) (lift h (minus d0 (S i)) w) (H2 x h (minus d0 (S i)) H12)) 
+(plus (S i) (minus d0 (S i))) (le_plus_minus (S i) d0 H4)) (lift h (plus (S 
+i) (minus d0 (S i))) (lift (S i) O w)) (lift_d w h (S i) (minus d0 (S i)) O 
+(le_O_n (minus d0 (S i))))) d0 (le_plus_minus_r (S i) d0 H4)) (lift h d0 
+(TLRef i)) (lift_lref_lt i h d0 H4))))) H10)))))))) H5))) (\lambda (H4: (le 
+d0 i)).(eq_ind_r T (TLRef (plus i h)) (\lambda (t: T).(sty0 g c0 t (lift h d0 
+(lift (S i) O w)))) (eq_ind nat (S i) (\lambda (_: nat).(sty0 g c0 (TLRef 
+(plus i h)) (lift h d0 (lift (S i) O w)))) (eq_ind_r T (lift (plus h (S i)) O 
+w) (\lambda (t: T).(sty0 g c0 (TLRef (plus i h)) t)) (eq_ind_r nat (plus (S 
+i) h) (\lambda (n: nat).(sty0 g c0 (TLRef (plus i h)) (lift n O w))) 
+(sty0_abbr g c0 d v (plus i h) (drop_getl_trans_ge i c0 c d0 h H3 (CHead d 
+(Bind Abbr) v) H0 H4) w H1) (plus h (S i)) (plus_sym h (S i))) (lift h d0 
+(lift (S i) O w)) (lift_free w (S i) h O d0 (le_S_n d0 (S i) (le_S (S d0) (S 
+i) (le_n_S d0 i H4))) (le_O_n d0))) (plus i (S O)) (eq_ind_r nat (plus (S O) 
+i) (\lambda (n: nat).(eq nat (S i) n)) (le_antisym (S i) (plus (S O) i) (le_n 
+(plus (S O) i)) (le_n (S i))) (plus i (S O)) (plus_sym i (S O)))) (lift h d0 
+(TLRef i)) (lift_lref_ge i h d0 H4)))))))))))))))) (\lambda (c: C).(\lambda 
+(d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d 
+(Bind Abst) v))).(\lambda (w: T).(\lambda (H1: (sty0 g d v w)).(\lambda (H2: 
+((\forall (c0: C).(\forall (h: nat).(\forall (d0: nat).((drop h d0 c0 d) \to 
+(sty0 g c0 (lift h d0 v) (lift h d0 w)))))))).(\lambda (c0: C).(\lambda (h: 
+nat).(\lambda (d0: nat).(\lambda (H3: (drop h d0 c0 c)).(lt_le_e i d0 (sty0 g 
+c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))) (\lambda (H4: (lt i 
+d0)).(let H5 \def (drop_getl_trans_le i d0 (le_S_n i d0 (le_S_n (S i) (S d0) 
+(le_S (S (S i)) (S d0) (le_n_S (S i) d0 H4)))) c0 c h H3 (CHead d (Bind Abst) 
+v) H0) in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_: C).(drop i O c0 e0))) 
 (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 i) e0 e1))) (\lambda (_: 
-C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abbr) v)))) (sty0 g c0 (lift h 
-d0 (TLRef i)) (lift h d0 (lift (S i) O w))) (\lambda (x0: C).(\lambda (x1: 
+C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abst) v)))) (sty0 g c0 (lift h 
+d0 (TLRef i)) (lift h d0 (lift (S i) O v))) (\lambda (x0: C).(\lambda (x1: 
 C).(\lambda (H6: (drop i O c0 x0)).(\lambda (H7: (drop h (minus d0 i) x0 
-x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abbr) v))).(let H9 \def (eq_ind 
+x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abst) v))).(let H9 \def (eq_ind 
 nat (minus d0 i) (\lambda (n: nat).(drop h n x0 x1)) H7 (S (minus d0 (S i))) 
 (minus_x_Sy d0 i H4)) in (let H10 \def (drop_clear_S x1 x0 h (minus d0 (S i)) 
-H9 Abbr d v H8) in (ex2_ind C (\lambda (c1: C).(clear x0 (CHead c1 (Bind 
-Abbr) (lift h (minus d0 (S i)) v)))) (\lambda (c1: C).(drop h (minus d0 (S 
-i)) c1 d)) (sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O w))) 
-(\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abbr) (lift h (minus 
+H9 Abst d v H8) in (ex2_ind C (\lambda (c1: C).(clear x0 (CHead c1 (Bind 
+Abst) (lift h (minus d0 (S i)) v)))) (\lambda (c1: C).(drop h (minus d0 (S 
+i)) c1 d)) (sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))) 
+(\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abst) (lift h (minus 
 d0 (S i)) v)))).(\lambda (H12: (drop h (minus d0 (S i)) x d)).(eq_ind_r T 
-(TLRef i) (\lambda (t: T).(sty0 g c0 t (lift h d0 (lift (S i) O w)))) (eq_ind 
+(TLRef i) (\lambda (t: T).(sty0 g c0 t (lift h d0 (lift (S i) O v)))) (eq_ind 
 nat (plus (S i) (minus d0 (S i))) (\lambda (n: nat).(sty0 g c0 (TLRef i) 
-(lift h n (lift (S i) O w)))) (eq_ind_r T (lift (S i) O (lift h (minus d0 (S 
-i)) w)) (\lambda (t: T).(sty0 g c0 (TLRef i) t)) (eq_ind nat d0 (\lambda (_: 
-nat).(sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) w)))) 
-(sty0_abbr g c0 x (lift h (minus d0 (S i)) v) i (getl_intro i c0 (CHead x 
-(Bind Abbr) (lift h (minus d0 (S i)) v)) x0 H6 H11) (lift h (minus d0 (S i)) 
+(lift h n (lift (S i) O v)))) (eq_ind_r T (lift (S i) O (lift h (minus d0 (S 
+i)) v)) (\lambda (t: T).(sty0 g c0 (TLRef i) t)) (eq_ind nat d0 (\lambda (_: 
+nat).(sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) v)))) 
+(sty0_abst g c0 x (lift h (minus d0 (S i)) v) i (getl_intro i c0 (CHead x 
+(Bind Abst) (lift h (minus d0 (S i)) v)) x0 H6 H11) (lift h (minus d0 (S i)) 
 w) (H2 x h (minus d0 (S i)) H12)) (plus (S i) (minus d0 (S i))) 
 (le_plus_minus (S i) d0 H4)) (lift h (plus (S i) (minus d0 (S i))) (lift (S 
-i) O w)) (lift_d w h (S i) (minus d0 (S i)) O (le_O_n (minus d0 (S i))))) d0 
-(le_plus_minus_r (S i) d0 H4)) (lift h d0 (TLRef i)) (lift_lref_lt i h d0 
-H4))))) H10)))))))) H5))) (\lambda (H4: (le d0 i)).(eq_ind_r T (TLRef (plus i 
-h)) (\lambda (t: T).(sty0 g c0 t (lift h d0 (lift (S i) O w)))) (eq_ind nat 
-(S i) (\lambda (_: nat).(sty0 g c0 (TLRef (plus i h)) (lift h d0 (lift (S i) 
-O w)))) (eq_ind_r T (lift (plus h (S i)) O w) (\lambda (t: T).(sty0 g c0 
-(TLRef (plus i h)) t)) (eq_ind_r nat (plus (S i) h) (\lambda (n: nat).(sty0 g 
-c0 (TLRef (plus i h)) (lift n O w))) (sty0_abbr g c0 d v (plus i h) 
-(drop_getl_trans_ge i c0 c d0 h H3 (CHead d (Bind Abbr) v) H0 H4) w H1) (plus 
-h (S i)) (plus_sym h (S i))) (lift h d0 (lift (S i) O w)) (lift_free w (S i) 
-h O d0 (le_S d0 i H4) (le_O_n d0))) (plus i (S O)) (eq_ind_r nat (plus (S O) 
-i) (\lambda (n: nat).(eq nat (S i) n)) (refl_equal nat (plus (S O) i)) (plus 
-i (S O)) (plus_sym i (S O)))) (lift h d0 (TLRef i)) (lift_lref_ge i h d0 
-H4)))))))))))))))) (\lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda 
-(i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abst) v))).(\lambda (w: 
-T).(\lambda (H1: (sty0 g d v w)).(\lambda (H2: ((\forall (c0: C).(\forall (h: 
-nat).(\forall (d0: nat).((drop h d0 c0 d) \to (sty0 g c0 (lift h d0 v) (lift 
-h d0 w)))))))).(\lambda (c0: C).(\lambda (h: nat).(\lambda (d0: nat).(\lambda 
-(H3: (drop h d0 c0 c)).(lt_le_e i d0 (sty0 g c0 (lift h d0 (TLRef i)) (lift h 
-d0 (lift (S i) O v))) (\lambda (H4: (lt i d0)).(let H5 \def 
-(drop_getl_trans_le i d0 (le_S_n i d0 (le_S (S i) d0 H4)) c0 c h H3 (CHead d 
-(Bind Abst) v) H0) in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_: C).(drop i 
-O c0 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 i) e0 e1))) 
-(\lambda (_: C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abst) v)))) (sty0 g 
-c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S i) O v))) (\lambda (x0: 
-C).(\lambda (x1: C).(\lambda (H6: (drop i O c0 x0)).(\lambda (H7: (drop h 
-(minus d0 i) x0 x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abst) v))).(let 
-H9 \def (eq_ind nat (minus d0 i) (\lambda (n: nat).(drop h n x0 x1)) H7 (S 
-(minus d0 (S i))) (minus_x_Sy d0 i H4)) in (let H10 \def (drop_clear_S x1 x0 
-h (minus d0 (S i)) H9 Abst d v H8) in (ex2_ind C (\lambda (c1: C).(clear x0 
-(CHead c1 (Bind Abst) (lift h (minus d0 (S i)) v)))) (\lambda (c1: C).(drop h 
-(minus d0 (S i)) c1 d)) (sty0 g c0 (lift h d0 (TLRef i)) (lift h d0 (lift (S 
-i) O v))) (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abst) (lift 
-h (minus d0 (S i)) v)))).(\lambda (H12: (drop h (minus d0 (S i)) x 
-d)).(eq_ind_r T (TLRef i) (\lambda (t: T).(sty0 g c0 t (lift h d0 (lift (S i) 
-O v)))) (eq_ind nat (plus (S i) (minus d0 (S i))) (\lambda (n: nat).(sty0 g 
-c0 (TLRef i) (lift h n (lift (S i) O v)))) (eq_ind_r T (lift (S i) O (lift h 
-(minus d0 (S i)) v)) (\lambda (t: T).(sty0 g c0 (TLRef i) t)) (eq_ind nat d0 
-(\lambda (_: nat).(sty0 g c0 (TLRef i) (lift (S i) O (lift h (minus d0 (S i)) 
-v)))) (sty0_abst g c0 x (lift h (minus d0 (S i)) v) i (getl_intro i c0 (CHead 
-x (Bind Abst) (lift h (minus d0 (S i)) v)) x0 H6 H11) (lift h (minus d0 (S 
-i)) w) (H2 x h (minus d0 (S i)) H12)) (plus (S i) (minus d0 (S i))) 
-(le_plus_minus (S i) d0 H4)) (lift h (plus (S i) (minus d0 (S i))) (lift (S 
 i) O v)) (lift_d v h (S i) (minus d0 (S i)) O (le_O_n (minus d0 (S i))))) d0 
 (le_plus_minus_r (S i) d0 H4)) (lift h d0 (TLRef i)) (lift_lref_lt i h d0 
 H4))))) H10)))))))) H5))) (\lambda (H4: (le d0 i)).(eq_ind_r T (TLRef (plus i 
@@ -115,12 +117,13 @@ O v)))) (eq_ind_r T (lift (plus h (S i)) O v) (\lambda (t: T).(sty0 g c0
 c0 (TLRef (plus i h)) (lift n O v))) (sty0_abst g c0 d v (plus i h) 
 (drop_getl_trans_ge i c0 c d0 h H3 (CHead d (Bind Abst) v) H0 H4) w H1) (plus 
 h (S i)) (plus_sym h (S i))) (lift h d0 (lift (S i) O v)) (lift_free v (S i) 
-h O d0 (le_S d0 i H4) (le_O_n d0))) (plus i (S O)) (eq_ind_r nat (plus (S O) 
-i) (\lambda (n: nat).(eq nat (S i) n)) (refl_equal nat (plus (S O) i)) (plus 
-i (S O)) (plus_sym i (S O)))) (lift h d0 (TLRef i)) (lift_lref_ge i h d0 
-H4)))))))))))))))) (\lambda (b: B).(\lambda (c: C).(\lambda (v: T).(\lambda 
-(t3: T).(\lambda (t4: T).(\lambda (_: (sty0 g (CHead c (Bind b) v) t3 
-t4)).(\lambda (H1: ((\forall (c0: C).(\forall (h: nat).(\forall (d: 
+h O d0 (le_S_n d0 (S i) (le_S (S d0) (S i) (le_n_S d0 i H4))) (le_O_n d0))) 
+(plus i (S O)) (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(eq nat (S i) 
+n)) (le_antisym (S i) (plus (S O) i) (le_n (plus (S O) i)) (le_n (S i))) 
+(plus i (S O)) (plus_sym i (S O)))) (lift h d0 (TLRef i)) (lift_lref_ge i h 
+d0 H4)))))))))))))))) (\lambda (b: B).(\lambda (c: C).(\lambda (v: 
+T).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (sty0 g (CHead c (Bind b) 
+v) t3 t4)).(\lambda (H1: ((\forall (c0: C).(\forall (h: nat).(\forall (d: 
 nat).((drop h d c0 (CHead c (Bind b) v)) \to (sty0 g c0 (lift h d t3) (lift h 
 d t4)))))))).(\lambda (c0: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda 
 (H2: (drop h d c0 c)).(eq_ind_r T (THead (Bind b) (lift h d v) (lift h (s 
@@ -159,9 +162,6 @@ h d H4) (lift h (s (Flat Cast) d) t3) (lift h (s (Flat Cast) d) t4) (H3 c0 h
 (s (Flat Cast) d) H4)) (lift h d (THead (Flat Cast) v2 t4)) (lift_head (Flat 
 Cast) v2 t4 h d)) (lift h d (THead (Flat Cast) v1 t3)) (lift_head (Flat Cast) 
 v1 t3 h d))))))))))))))) e t1 t2 H))))).
-(* COMMENTS
-Initial nodes: 3677
-END *)
 
 theorem sty0_correct:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty0 g c 
@@ -211,7 +211,4 @@ T).(sty0 g c0 (THead (Flat Cast) v2 t3) t4))) (\lambda (x0: T).(\lambda (H7:
 (sty0 g c0 t3 x0)).(ex_intro T (\lambda (t4: T).(sty0 g c0 (THead (Flat Cast) 
 v2 t3) t4)) (THead (Flat Cast) x x0) (sty0_cast g c0 v2 x H5 t3 x0 H7)))) 
 H6)))) H4))))))))))) c t1 t H))))).
-(* COMMENTS
-Initial nodes: 991
-END *)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma b/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma
index 0f39bdfd93b0cbdc61159f871bef58435c3f8496..82448bfcae79fbd35559b4c40be42baf3fdbd0fa 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty1/cnt.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/sty1/props.ma".
+include "basic_1/sty1/props.ma".
 
-include "Basic-1/cnt/props.ma".
+include "basic_1/cnt/props.ma".
 
 theorem sty1_cnt:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty0 g c 
@@ -24,66 +24,111 @@ t1 t) \to (ex2 T (\lambda (t2: T).(sty1 g c t1 t2)) (\lambda (t2: T).(cnt
 t2)))))))
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (t: T).(\lambda (H: 
-(sty0 g c t1 t)).(sty0_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (_: 
-T).(ex2 T (\lambda (t3: T).(sty1 g c0 t0 t3)) (\lambda (t3: T).(cnt t3)))))) 
-(\lambda (c0: C).(\lambda (n: nat).(ex_intro2 T (\lambda (t2: T).(sty1 g c0 
-(TSort n) t2)) (\lambda (t2: T).(cnt t2)) (TSort (next g n)) (sty1_sty0 g c0 
-(TSort n) (TSort (next g n)) (sty0_sort g c0 n)) (cnt_sort (next g n))))) 
-(\lambda (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda 
-(H0: (getl i c0 (CHead d (Bind Abbr) v))).(\lambda (w: T).(\lambda (_: (sty0 
-g d v w)).(\lambda (H2: (ex2 T (\lambda (t2: T).(sty1 g d v t2)) (\lambda 
-(t2: T).(cnt t2)))).(let H3 \def H2 in (ex2_ind T (\lambda (t2: T).(sty1 g d 
-v t2)) (\lambda (t2: T).(cnt t2)) (ex2 T (\lambda (t2: T).(sty1 g c0 (TLRef 
-i) t2)) (\lambda (t2: T).(cnt t2))) (\lambda (x: T).(\lambda (H4: (sty1 g d v 
-x)).(\lambda (H5: (cnt x)).(ex_intro2 T (\lambda (t2: T).(sty1 g c0 (TLRef i) 
-t2)) (\lambda (t2: T).(cnt t2)) (lift (S i) O x) (sty1_abbr g c0 d v i H0 x 
-H4) (cnt_lift x H5 (S i) O))))) H3)))))))))) (\lambda (c0: C).(\lambda (d: 
+(sty0 g c t1 t)).(let TMP_3 \def (\lambda (c0: C).(\lambda (t0: T).(\lambda 
+(_: T).(let TMP_1 \def (\lambda (t3: T).(sty1 g c0 t0 t3)) in (let TMP_2 \def 
+(\lambda (t3: T).(cnt t3)) in (ex2 T TMP_1 TMP_2)))))) in (let TMP_16 \def 
+(\lambda (c0: C).(\lambda (n: nat).(let TMP_5 \def (\lambda (t2: T).(let 
+TMP_4 \def (TSort n) in (sty1 g c0 TMP_4 t2))) in (let TMP_6 \def (\lambda 
+(t2: T).(cnt t2)) in (let TMP_7 \def (next g n) in (let TMP_8 \def (TSort 
+TMP_7) in (let TMP_9 \def (TSort n) in (let TMP_10 \def (next g n) in (let 
+TMP_11 \def (TSort TMP_10) in (let TMP_12 \def (sty0_sort g c0 n) in (let 
+TMP_13 \def (sty1_sty0 g c0 TMP_9 TMP_11 TMP_12) in (let TMP_14 \def (next g 
+n) in (let TMP_15 \def (cnt_sort TMP_14) in (ex_intro2 T TMP_5 TMP_6 TMP_8 
+TMP_13 TMP_15)))))))))))))) in (let TMP_32 \def (\lambda (c0: C).(\lambda (d: 
 C).(\lambda (v: T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind 
-Abst) v))).(\lambda (w: T).(\lambda (H1: (sty0 g d v w)).(\lambda (H2: (ex2 T 
+Abbr) v))).(\lambda (w: T).(\lambda (_: (sty0 g d v w)).(\lambda (H2: (ex2 T 
 (\lambda (t2: T).(sty1 g d v t2)) (\lambda (t2: T).(cnt t2)))).(let H3 \def 
-H2 in (ex2_ind T (\lambda (t2: T).(sty1 g d v t2)) (\lambda (t2: T).(cnt t2)) 
-(ex2 T (\lambda (t2: T).(sty1 g c0 (TLRef i) t2)) (\lambda (t2: T).(cnt t2))) 
-(\lambda (x: T).(\lambda (H4: (sty1 g d v x)).(\lambda (H5: (cnt 
-x)).(ex_intro2 T (\lambda (t2: T).(sty1 g c0 (TLRef i) t2)) (\lambda (t2: 
-T).(cnt t2)) (lift (S i) O x) (sty1_trans g c0 (TLRef i) (lift (S i) O v) 
-(sty1_sty0 g c0 (TLRef i) (lift (S i) O v) (sty0_abst g c0 d v i H0 w H1)) 
-(lift (S i) O x) (sty1_lift g d v x H4 c0 (S i) O (getl_drop Abst c0 d v i 
-H0))) (cnt_lift x H5 (S i) O))))) H3)))))))))) (\lambda (b: B).(\lambda (c0: 
+H2 in (let TMP_17 \def (\lambda (t2: T).(sty1 g d v t2)) in (let TMP_18 \def 
+(\lambda (t2: T).(cnt t2)) in (let TMP_20 \def (\lambda (t2: T).(let TMP_19 
+\def (TLRef i) in (sty1 g c0 TMP_19 t2))) in (let TMP_21 \def (\lambda (t2: 
+T).(cnt t2)) in (let TMP_22 \def (ex2 T TMP_20 TMP_21) in (let TMP_31 \def 
+(\lambda (x: T).(\lambda (H4: (sty1 g d v x)).(\lambda (H5: (cnt x)).(let 
+TMP_24 \def (\lambda (t2: T).(let TMP_23 \def (TLRef i) in (sty1 g c0 TMP_23 
+t2))) in (let TMP_25 \def (\lambda (t2: T).(cnt t2)) in (let TMP_26 \def (S 
+i) in (let TMP_27 \def (lift TMP_26 O x) in (let TMP_28 \def (sty1_abbr g c0 
+d v i H0 x H4) in (let TMP_29 \def (S i) in (let TMP_30 \def (cnt_lift x H5 
+TMP_29 O) in (ex_intro2 T TMP_24 TMP_25 TMP_27 TMP_28 TMP_30))))))))))) in 
+(ex2_ind T TMP_17 TMP_18 TMP_22 TMP_31 H3)))))))))))))))) in (let TMP_61 \def 
+(\lambda (c0: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda 
+(H0: (getl i c0 (CHead d (Bind Abst) v))).(\lambda (w: T).(\lambda (H1: (sty0 
+g d v w)).(\lambda (H2: (ex2 T (\lambda (t2: T).(sty1 g d v t2)) (\lambda 
+(t2: T).(cnt t2)))).(let H3 \def H2 in (let TMP_33 \def (\lambda (t2: 
+T).(sty1 g d v t2)) in (let TMP_34 \def (\lambda (t2: T).(cnt t2)) in (let 
+TMP_36 \def (\lambda (t2: T).(let TMP_35 \def (TLRef i) in (sty1 g c0 TMP_35 
+t2))) in (let TMP_37 \def (\lambda (t2: T).(cnt t2)) in (let TMP_38 \def (ex2 
+T TMP_36 TMP_37) in (let TMP_60 \def (\lambda (x: T).(\lambda (H4: (sty1 g d 
+v x)).(\lambda (H5: (cnt x)).(let TMP_40 \def (\lambda (t2: T).(let TMP_39 
+\def (TLRef i) in (sty1 g c0 TMP_39 t2))) in (let TMP_41 \def (\lambda (t2: 
+T).(cnt t2)) in (let TMP_42 \def (S i) in (let TMP_43 \def (lift TMP_42 O x) 
+in (let TMP_44 \def (TLRef i) in (let TMP_45 \def (S i) in (let TMP_46 \def 
+(lift TMP_45 O v) in (let TMP_47 \def (TLRef i) in (let TMP_48 \def (S i) in 
+(let TMP_49 \def (lift TMP_48 O v) in (let TMP_50 \def (sty0_abst g c0 d v i 
+H0 w H1) in (let TMP_51 \def (sty1_sty0 g c0 TMP_47 TMP_49 TMP_50) in (let 
+TMP_52 \def (S i) in (let TMP_53 \def (lift TMP_52 O x) in (let TMP_54 \def 
+(S i) in (let TMP_55 \def (getl_drop Abst c0 d v i H0) in (let TMP_56 \def 
+(sty1_lift g d v x H4 c0 TMP_54 O TMP_55) in (let TMP_57 \def (sty1_trans g 
+c0 TMP_44 TMP_46 TMP_51 TMP_53 TMP_56) in (let TMP_58 \def (S i) in (let 
+TMP_59 \def (cnt_lift x H5 TMP_58 O) in (ex_intro2 T TMP_40 TMP_41 TMP_43 
+TMP_57 TMP_59)))))))))))))))))))))))) in (ex2_ind T TMP_33 TMP_34 TMP_38 
+TMP_60 H3)))))))))))))))) in (let TMP_81 \def (\lambda (b: B).(\lambda (c0: 
 C).(\lambda (v: T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (sty0 g 
 (CHead c0 (Bind b) v) t2 t3)).(\lambda (H1: (ex2 T (\lambda (t4: T).(sty1 g 
 (CHead c0 (Bind b) v) t2 t4)) (\lambda (t4: T).(cnt t4)))).(let H2 \def H1 in 
-(ex2_ind T (\lambda (t4: T).(sty1 g (CHead c0 (Bind b) v) t2 t4)) (\lambda 
-(t4: T).(cnt t4)) (ex2 T (\lambda (t4: T).(sty1 g c0 (THead (Bind b) v t2) 
-t4)) (\lambda (t4: T).(cnt t4))) (\lambda (x: T).(\lambda (H3: (sty1 g (CHead 
-c0 (Bind b) v) t2 x)).(\lambda (H4: (cnt x)).(ex_intro2 T (\lambda (t4: 
-T).(sty1 g c0 (THead (Bind b) v t2) t4)) (\lambda (t4: T).(cnt t4)) (THead 
-(Bind b) v x) (sty1_bind g b c0 v t2 x H3) (cnt_head x H4 (Bind b) v))))) 
-H2))))))))) (\lambda (c0: C).(\lambda (v: T).(\lambda (t2: T).(\lambda (t3: 
-T).(\lambda (_: (sty0 g c0 t2 t3)).(\lambda (H1: (ex2 T (\lambda (t4: 
-T).(sty1 g c0 t2 t4)) (\lambda (t4: T).(cnt t4)))).(let H2 \def H1 in 
-(ex2_ind T (\lambda (t4: T).(sty1 g c0 t2 t4)) (\lambda (t4: T).(cnt t4)) 
-(ex2 T (\lambda (t4: T).(sty1 g c0 (THead (Flat Appl) v t2) t4)) (\lambda 
-(t4: T).(cnt t4))) (\lambda (x: T).(\lambda (H3: (sty1 g c0 t2 x)).(\lambda 
-(H4: (cnt x)).(ex_intro2 T (\lambda (t4: T).(sty1 g c0 (THead (Flat Appl) v 
-t2) t4)) (\lambda (t4: T).(cnt t4)) (THead (Flat Appl) v x) (sty1_appl g c0 v 
-t2 x H3) (cnt_head x H4 (Flat Appl) v))))) H2)))))))) (\lambda (c0: 
-C).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H0: (sty0 g c0 v1 
-v2)).(\lambda (_: (ex2 T (\lambda (t2: T).(sty1 g c0 v1 t2)) (\lambda (t2: 
-T).(cnt t2)))).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (sty0 g c0 t2 
-t3)).(\lambda (H3: (ex2 T (\lambda (t4: T).(sty1 g c0 t2 t4)) (\lambda (t4: 
-T).(cnt t4)))).(let H4 \def H3 in (ex2_ind T (\lambda (t4: T).(sty1 g c0 t2 
-t4)) (\lambda (t4: T).(cnt t4)) (ex2 T (\lambda (t4: T).(sty1 g c0 (THead 
-(Flat Cast) v1 t2) t4)) (\lambda (t4: T).(cnt t4))) (\lambda (x: T).(\lambda 
-(H5: (sty1 g c0 t2 x)).(\lambda (H6: (cnt x)).(let H_x \def (sty1_cast2 g c0 
-t2 x H5 v1 v2 H0) in (let H7 \def H_x in (ex2_ind T (\lambda (v3: T).(sty1 g 
-c0 v1 v3)) (\lambda (v3: T).(sty1 g c0 (THead (Flat Cast) v1 t2) (THead (Flat 
-Cast) v3 x))) (ex2 T (\lambda (t4: T).(sty1 g c0 (THead (Flat Cast) v1 t2) 
-t4)) (\lambda (t4: T).(cnt t4))) (\lambda (x0: T).(\lambda (_: (sty1 g c0 v1 
-x0)).(\lambda (H9: (sty1 g c0 (THead (Flat Cast) v1 t2) (THead (Flat Cast) x0 
-x))).(ex_intro2 T (\lambda (t4: T).(sty1 g c0 (THead (Flat Cast) v1 t2) t4)) 
-(\lambda (t4: T).(cnt t4)) (THead (Flat Cast) x0 x) H9 (cnt_head x H6 (Flat 
-Cast) x0))))) H7)))))) H4))))))))))) c t1 t H))))).
-(* COMMENTS
-Initial nodes: 1313
-END *)
+(let TMP_64 \def (\lambda (t4: T).(let TMP_62 \def (Bind b) in (let TMP_63 
+\def (CHead c0 TMP_62 v) in (sty1 g TMP_63 t2 t4)))) in (let TMP_65 \def 
+(\lambda (t4: T).(cnt t4)) in (let TMP_68 \def (\lambda (t4: T).(let TMP_66 
+\def (Bind b) in (let TMP_67 \def (THead TMP_66 v t2) in (sty1 g c0 TMP_67 
+t4)))) in (let TMP_69 \def (\lambda (t4: T).(cnt t4)) in (let TMP_70 \def 
+(ex2 T TMP_68 TMP_69) in (let TMP_80 \def (\lambda (x: T).(\lambda (H3: (sty1 
+g (CHead c0 (Bind b) v) t2 x)).(\lambda (H4: (cnt x)).(let TMP_73 \def 
+(\lambda (t4: T).(let TMP_71 \def (Bind b) in (let TMP_72 \def (THead TMP_71 
+v t2) in (sty1 g c0 TMP_72 t4)))) in (let TMP_74 \def (\lambda (t4: T).(cnt 
+t4)) in (let TMP_75 \def (Bind b) in (let TMP_76 \def (THead TMP_75 v x) in 
+(let TMP_77 \def (sty1_bind g b c0 v t2 x H3) in (let TMP_78 \def (Bind b) in 
+(let TMP_79 \def (cnt_head x H4 TMP_78 v) in (ex_intro2 T TMP_73 TMP_74 
+TMP_76 TMP_77 TMP_79))))))))))) in (ex2_ind T TMP_64 TMP_65 TMP_70 TMP_80 
+H2))))))))))))))) in (let TMP_99 \def (\lambda (c0: C).(\lambda (v: 
+T).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (sty0 g c0 t2 t3)).(\lambda 
+(H1: (ex2 T (\lambda (t4: T).(sty1 g c0 t2 t4)) (\lambda (t4: T).(cnt 
+t4)))).(let H2 \def H1 in (let TMP_82 \def (\lambda (t4: T).(sty1 g c0 t2 
+t4)) in (let TMP_83 \def (\lambda (t4: T).(cnt t4)) in (let TMP_86 \def 
+(\lambda (t4: T).(let TMP_84 \def (Flat Appl) in (let TMP_85 \def (THead 
+TMP_84 v t2) in (sty1 g c0 TMP_85 t4)))) in (let TMP_87 \def (\lambda (t4: 
+T).(cnt t4)) in (let TMP_88 \def (ex2 T TMP_86 TMP_87) in (let TMP_98 \def 
+(\lambda (x: T).(\lambda (H3: (sty1 g c0 t2 x)).(\lambda (H4: (cnt x)).(let 
+TMP_91 \def (\lambda (t4: T).(let TMP_89 \def (Flat Appl) in (let TMP_90 \def 
+(THead TMP_89 v t2) in (sty1 g c0 TMP_90 t4)))) in (let TMP_92 \def (\lambda 
+(t4: T).(cnt t4)) in (let TMP_93 \def (Flat Appl) in (let TMP_94 \def (THead 
+TMP_93 v x) in (let TMP_95 \def (sty1_appl g c0 v t2 x H3) in (let TMP_96 
+\def (Flat Appl) in (let TMP_97 \def (cnt_head x H4 TMP_96 v) in (ex_intro2 T 
+TMP_91 TMP_92 TMP_94 TMP_95 TMP_97))))))))))) in (ex2_ind T TMP_82 TMP_83 
+TMP_88 TMP_98 H2)))))))))))))) in (let TMP_128 \def (\lambda (c0: C).(\lambda 
+(v1: T).(\lambda (v2: T).(\lambda (H0: (sty0 g c0 v1 v2)).(\lambda (_: (ex2 T 
+(\lambda (t2: T).(sty1 g c0 v1 t2)) (\lambda (t2: T).(cnt t2)))).(\lambda 
+(t2: T).(\lambda (t3: T).(\lambda (_: (sty0 g c0 t2 t3)).(\lambda (H3: (ex2 T 
+(\lambda (t4: T).(sty1 g c0 t2 t4)) (\lambda (t4: T).(cnt t4)))).(let H4 \def 
+H3 in (let TMP_100 \def (\lambda (t4: T).(sty1 g c0 t2 t4)) in (let TMP_101 
+\def (\lambda (t4: T).(cnt t4)) in (let TMP_104 \def (\lambda (t4: T).(let 
+TMP_102 \def (Flat Cast) in (let TMP_103 \def (THead TMP_102 v1 t2) in (sty1 
+g c0 TMP_103 t4)))) in (let TMP_105 \def (\lambda (t4: T).(cnt t4)) in (let 
+TMP_106 \def (ex2 T TMP_104 TMP_105) in (let TMP_127 \def (\lambda (x: 
+T).(\lambda (H5: (sty1 g c0 t2 x)).(\lambda (H6: (cnt x)).(let H_x \def 
+(sty1_cast2 g c0 t2 x H5 v1 v2 H0) in (let H7 \def H_x in (let TMP_107 \def 
+(\lambda (v3: T).(sty1 g c0 v1 v3)) in (let TMP_112 \def (\lambda (v3: 
+T).(let TMP_108 \def (Flat Cast) in (let TMP_109 \def (THead TMP_108 v1 t2) 
+in (let TMP_110 \def (Flat Cast) in (let TMP_111 \def (THead TMP_110 v3 x) in 
+(sty1 g c0 TMP_109 TMP_111)))))) in (let TMP_115 \def (\lambda (t4: T).(let 
+TMP_113 \def (Flat Cast) in (let TMP_114 \def (THead TMP_113 v1 t2) in (sty1 
+g c0 TMP_114 t4)))) in (let TMP_116 \def (\lambda (t4: T).(cnt t4)) in (let 
+TMP_117 \def (ex2 T TMP_115 TMP_116) in (let TMP_126 \def (\lambda (x0: 
+T).(\lambda (_: (sty1 g c0 v1 x0)).(\lambda (H9: (sty1 g c0 (THead (Flat 
+Cast) v1 t2) (THead (Flat Cast) x0 x))).(let TMP_120 \def (\lambda (t4: 
+T).(let TMP_118 \def (Flat Cast) in (let TMP_119 \def (THead TMP_118 v1 t2) 
+in (sty1 g c0 TMP_119 t4)))) in (let TMP_121 \def (\lambda (t4: T).(cnt t4)) 
+in (let TMP_122 \def (Flat Cast) in (let TMP_123 \def (THead TMP_122 x0 x) in 
+(let TMP_124 \def (Flat Cast) in (let TMP_125 \def (cnt_head x H6 TMP_124 x0) 
+in (ex_intro2 T TMP_120 TMP_121 TMP_123 H9 TMP_125)))))))))) in (ex2_ind T 
+TMP_107 TMP_112 TMP_117 TMP_126 H7)))))))))))) in (ex2_ind T TMP_100 TMP_101 
+TMP_106 TMP_127 H4))))))))))))))))) in (sty0_ind g TMP_3 TMP_16 TMP_32 TMP_61 
+TMP_81 TMP_99 TMP_128 c t1 t H)))))))))))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty1/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/sty1/defs.ma
index 8fd219524e3e62355fed51a5ac02f0f4542003c7..9b98d8a562dd052c478c8d4f0f799cd193fea545 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/sty1/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty1/defs.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/sty0/defs.ma".
+include "basic_1/sty0/defs.ma".
 
 inductive sty1 (g: G) (c: C) (t1: T): T \to Prop \def
 | sty1_sty0: \forall (t2: T).((sty0 g c t1 t2) \to (sty1 g c t1 t2))

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty1/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/sty1/fwd.ma
new file mode 100644 (file)
index 0000000..f6680fc
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty1/fwd.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "basic_1/sty1/defs.ma".
+
+let rec sty1_ind (g: G) (c: C) (t1: T) (P: (T \to Prop)) (f: (\forall (t2: 
+T).((sty0 g c t1 t2) \to (P t2)))) (f0: (\forall (t: T).((sty1 g c t1 t) \to 
+((P t) \to (\forall (t2: T).((sty0 g c t t2) \to (P t2))))))) (t: T) (s0: 
+sty1 g c t1 t) on s0: P t \def match s0 with [(sty1_sty0 t2 s1) \Rightarrow 
+(f t2 s1) | (sty1_sing t0 s1 t2 s2) \Rightarrow (f0 t0 s1 ((sty1_ind g c t1 P 
+f f0) t0 s1) t2 s2)].
+

diff --git a/matita/matita/contribs/lambdadelta/basic_1/sty1/props.ma b/matita/matita/contribs/lambdadelta/basic_1/sty1/props.ma
index 53061952e312717dc04c55fe970e84d04ff9e8c4..46a807164378144319309e68a3b6fd3bd97db14d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/sty1/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/sty1/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/sty1/defs.ma".
+include "basic_1/sty1/fwd.ma".
 
-include "Basic-1/sty0/props.ma".
+include "basic_1/sty0/props.ma".
 
 theorem sty1_trans:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty1 g c 
@@ -28,9 +28,6 @@ c t (\lambda (t0: T).(sty1 g c t1 t0)) (\lambda (t3: T).(\lambda (H1: (sty0 g
 c t t3)).(sty1_sing g c t1 t H t3 H1))) (\lambda (t0: T).(\lambda (_: (sty1 g 
 c t t0)).(\lambda (H2: (sty1 g c t1 t0)).(\lambda (t3: T).(\lambda (H3: (sty0 
 g c t0 t3)).(sty1_sing g c t1 t0 H2 t3 H3)))))) t2 H0))))))).
-(* COMMENTS
-Initial nodes: 131
-END *)
 
 theorem sty1_bind:
  \forall (g: G).(\forall (b: B).(\forall (c: C).(\forall (v: T).(\forall (t1: 
@@ -47,9 +44,6 @@ t2)).(sty1_ind g (CHead c (Bind b) v) t1 (\lambda (t: T).(sty1 g c (THead
 t1) (THead (Bind b) v t))).(\lambda (t3: T).(\lambda (H2: (sty0 g (CHead c 
 (Bind b) v) t t3)).(sty1_sing g c (THead (Bind b) v t1) (THead (Bind b) v t) 
 H1 (THead (Bind b) v t3) (sty0_bind g b c v t t3 H2))))))) t2 H))))))).
-(* COMMENTS
-Initial nodes: 259
-END *)
 
 theorem sty1_appl:
  \forall (g: G).(\forall (c: C).(\forall (v: T).(\forall (t1: T).(\forall 
@@ -65,9 +59,6 @@ T).(\lambda (_: (sty1 g c t1 t)).(\lambda (H1: (sty1 g c (THead (Flat Appl) v
 t1) (THead (Flat Appl) v t))).(\lambda (t3: T).(\lambda (H2: (sty0 g c t 
 t3)).(sty1_sing g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t) H1 
 (THead (Flat Appl) v t3) (sty0_appl g c v t t3 H2))))))) t2 H)))))).
-(* COMMENTS
-Initial nodes: 213
-END *)
 
 theorem sty1_lift:
  \forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((sty1 g e 
@@ -86,9 +77,6 @@ c h d H1)))))))) (\lambda (t: T).(\lambda (_: (sty1 g e t1 t)).(\lambda (H1:
 (sty0 g e t t3)).(\lambda (c: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda 
 (H3: (drop h d c e)).(sty1_sing g c (lift h d t1) (lift h d t) (H1 c h d H3) 
 (lift h d t3) (sty0_lift g e t t3 H2 c h d H3))))))))))) t2 H))))).
-(* COMMENTS
-Initial nodes: 277
-END *)
 
 theorem sty1_correct:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t: T).((sty1 g c 
@@ -100,9 +88,6 @@ T).(sty0 g c t0 t2)))) (\lambda (t2: T).(\lambda (H0: (sty0 g c t1
 t2)).(sty0_correct g c t1 t2 H0))) (\lambda (t0: T).(\lambda (_: (sty1 g c t1 
 t0)).(\lambda (_: (ex T (\lambda (t2: T).(sty0 g c t0 t2)))).(\lambda (t2: 
 T).(\lambda (H2: (sty0 g c t0 t2)).(sty0_correct g c t0 t2 H2)))))) t H))))).
-(* COMMENTS
-Initial nodes: 123
-END *)
 
 theorem sty1_abbr:
  \forall (g: G).(\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: 
@@ -119,9 +104,6 @@ H1)))) (\lambda (t: T).(\lambda (_: (sty1 g d v t)).(\lambda (H2: (sty1 g c
 t2)).(sty1_sing g c (TLRef i) (lift (S i) O t) H2 (lift (S i) O t2) 
 (sty0_lift g d t t2 H3 c (S i) O (getl_drop Abbr c d v i H)))))))) w 
 H0)))))))).
-(* COMMENTS
-Initial nodes: 231
-END *)
 
 theorem sty1_cast2:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((sty1 g c 
@@ -157,7 +139,4 @@ c v1 v3)) (\lambda (v3: T).(sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat
 Cast) v3 t3))) x0 (sty1_sing g c v1 x H5 x0 H8) (sty1_sing g c (THead (Flat 
 Cast) v1 t1) (THead (Flat Cast) x t) H6 (THead (Flat Cast) x0 t3) (sty0_cast 
 g c x x0 H8 t t3 H2))))) H7)))))) H4))))))))))) t2 H))))).
-(* COMMENTS
-Initial nodes: 657
-END *)