basic_1: COMMIT COMPLETED

- component wf3
- additional files
basic_2: some corrections

diff --git a/matita/matita/contribs/lambdadelta/basic_1/definitions.ma b/matita/matita/contribs/lambdadelta/basic_1/definitions.ma
index 5863b424310a8b3c52d0997667c439a8d1d85e5d..010b9d252948eca6b9d76362e066f0b9b25b779b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/definitions.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/definitions.ma
@@ -14,55 +14,55 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/tlt/defs.ma".
+include "basic_1/tlt/defs.ma".
 
-include "Basic-1/iso/defs.ma".
+include "basic_1/iso/defs.ma".
 
-include "Basic-1/clen/defs.ma".
+include "basic_1/clen/defs.ma".
 
-include "Basic-1/flt/defs.ma".
+include "basic_1/flt/defs.ma".
 
-include "Basic-1/app/defs.ma".
+include "basic_1/app/defs.ma".
 
-include "Basic-1/cnt/defs.ma".
+include "basic_1/cnt/defs.ma".
 
-include "Basic-1/cimp/defs.ma".
+include "basic_1/cimp/defs.ma".
 
-include "Basic-1/csubv/defs.ma".
+include "basic_1/subst1/defs.ma".
 
-include "Basic-1/subst/defs.ma".
+include "basic_1/subst/defs.ma".
 
-include "Basic-1/subst1/defs.ma".
+include "basic_1/csubst1/defs.ma".
 
-include "Basic-1/csubst1/defs.ma".
+include "basic_1/fsubst0/defs.ma".
 
-include "Basic-1/fsubst0/defs.ma".
+include "basic_1/next_plus/defs.ma".
 
-include "Basic-1/next_plus/defs.ma".
+include "basic_1/sty1/defs.ma".
 
-include "Basic-1/sty1/defs.ma".
+include "basic_1/llt/defs.ma".
 
-include "Basic-1/llt/defs.ma".
+include "basic_1/aprem/defs.ma".
 
-include "Basic-1/aprem/defs.ma".
+include "basic_1/ex0/defs.ma".
 
-include "Basic-1/ex0/defs.ma".
+include "basic_1/wcpr0/defs.ma".
 
-include "Basic-1/wcpr0/defs.ma".
+include "basic_1/csubv/defs.ma".
 
-include "Basic-1/csuba/defs.ma".
+include "basic_1/csuba/defs.ma".
 
-include "Basic-1/nf2/defs.ma".
+include "basic_1/nf2/defs.ma".
 
-include "Basic-1/ex2/defs.ma".
+include "basic_1/ex2/defs.ma".
 
-include "Basic-1/csubc/defs.ma".
+include "basic_1/csubc/defs.ma".
 
-include "Basic-1/pc1/defs.ma".
+include "basic_1/pc1/defs.ma".
 
-include "Basic-1/ex1/defs.ma".
+include "basic_1/ex1/defs.ma".
 
-include "Basic-1/csubt/defs.ma".
+include "basic_1/csubt/defs.ma".
 
-include "Basic-1/wf3/defs.ma".
+include "basic_1/wf3/defs.ma".
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/planes.txt b/matita/matita/contribs/lambdadelta/basic_1/planes.txt
new file mode 100644 (file)
index 0000000..d4b66b3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_1/planes.txt
@@ -0,0 +1,13 @@
+T s tlist tlt iso
+C r flt app
+lift cnt drop clear getl clen cimp
+lift1 drop1
+subst0 subst1 subst csubst0 csubst1 fsubst0 
+G next_plus
+sty0 sty1
+A asucc aplus leq llt aprem ex0 
+pr0 wcpr0 pr1 pr2 pr3 
+csubv arity csuba
+nf2 sn3 sc3 csubc ex2
+pc1 pc3
+ty3 csubt wf3 ex1

diff --git a/matita/matita/contribs/lambdadelta/basic_1/spare.ma b/matita/matita/contribs/lambdadelta/basic_1/spare.ma
index 95d2c24eec87439535012c2078809264a977a730..58a624eef400442cdb2035ed8b39114fecb2503f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/spare.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/spare.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/theory.ma".
+include "basic_1/theory.ma".
 
 axiom pc3_gen_appls_sort_abst:
  \forall (c: C).(\forall (vs: TList).(\forall (w: T).(\forall (u: T).(\forall 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/theory.ma b/matita/matita/contribs/lambdadelta/basic_1/theory.ma
index f405be588d3dc75a1d036a7f9a3b6c28f34e4d8a..771c60e75fd5b10c07a76a00e9c4b69e74980b12 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/theory.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/theory.ma
@@ -14,29 +14,27 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/subst0/tlt.ma".
+include "basic_1/subst0/tlt.ma".
 
-include "Basic-1/subst/props.ma".
+include "basic_1/subst/props.ma".
 
-include "Basic-1/sty1/cnt.ma".
+include "basic_1/sty1/cnt.ma".
 
-include "Basic-1/ex0/props.ma".
+include "basic_1/ex0/props.ma".
 
-include "Basic-1/wcpr0/fwd.ma".
+include "basic_1/pr3/wcpr0.ma".
 
-include "Basic-1/pr3/wcpr0.ma".
+include "basic_1/ex2/props.ma".
 
-include "Basic-1/ex2/props.ma".
+include "basic_1/ex1/props.ma".
 
-include "Basic-1/ex1/props.ma".
+include "basic_1/ty3/sty0.ma".
 
-include "Basic-1/ty3/sty0.ma".
+include "basic_1/csubt/csuba.ma".
 
-include "Basic-1/csubt/csuba.ma".
+include "basic_1/ty3/fwd_nf2.ma".
 
-include "Basic-1/ty3/fwd_nf2.ma".
+include "basic_1/ty3/nf2.ma".
 
-include "Basic-1/ty3/nf2.ma".
-
-include "Basic-1/wf3/props.ma".
+include "basic_1/wf3/props.ma".
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/clear.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/clear.ma
index b2ddd47af9c12718e6d86eab6ca6aaec2bb8c36c..4eb5de99c50a6446f33428d608e088c59f32bba7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/wf3/clear.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/clear.ma
@@ -14,78 +14,113 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/wf3/fwd.ma".
+include "basic_1/wf3/fwd.ma".
+
+include "basic_1/clear/fwd.ma".
 
 theorem wf3_clear_conf:
  \forall (c1: C).(\forall (c: C).((clear c1 c) \to (\forall (g: G).(\forall 
 (c2: C).((wf3 g c1 c2) \to (wf3 g c c2))))))
 \def
- \lambda (c1: C).(\lambda (c: C).(\lambda (H: (clear c1 c)).(clear_ind 
+ \lambda (c1: C).(\lambda (c: C).(\lambda (H: (clear c1 c)).(let TMP_1 \def 
 (\lambda (c0: C).(\lambda (c2: C).(\forall (g: G).(\forall (c3: C).((wf3 g c0 
-c3) \to (wf3 g c2 c3)))))) (\lambda (b: B).(\lambda (e: C).(\lambda (u: 
-T).(\lambda (g: G).(\lambda (c2: C).(\lambda (H0: (wf3 g (CHead e (Bind b) u) 
-c2)).H0)))))) (\lambda (e: C).(\lambda (c0: C).(\lambda (_: (clear e 
-c0)).(\lambda (H1: ((\forall (g: G).(\forall (c2: C).((wf3 g e c2) \to (wf3 g 
-c0 c2)))))).(\lambda (f: F).(\lambda (u: T).(\lambda (g: G).(\lambda (c2: 
-C).(\lambda (H2: (wf3 g (CHead e (Flat f) u) c2)).(let H_y \def 
-(wf3_gen_flat1 g e c2 u f H2) in (H1 g c2 H_y))))))))))) c1 c H))).
-(* COMMENTS
-Initial nodes: 145
-END *)
+c3) \to (wf3 g c2 c3)))))) in (let TMP_2 \def (\lambda (b: B).(\lambda (e: 
+C).(\lambda (u: T).(\lambda (g: G).(\lambda (c2: C).(\lambda (H0: (wf3 g 
+(CHead e (Bind b) u) c2)).H0)))))) in (let TMP_3 \def (\lambda (e: 
+C).(\lambda (c0: C).(\lambda (_: (clear e c0)).(\lambda (H1: ((\forall (g: 
+G).(\forall (c2: C).((wf3 g e c2) \to (wf3 g c0 c2)))))).(\lambda (f: 
+F).(\lambda (u: T).(\lambda (g: G).(\lambda (c2: C).(\lambda (H2: (wf3 g 
+(CHead e (Flat f) u) c2)).(let H_y \def (wf3_gen_flat1 g e c2 u f H2) in (H1 
+g c2 H_y))))))))))) in (clear_ind TMP_1 TMP_2 TMP_3 c1 c H)))))).
 
 theorem clear_wf3_trans:
  \forall (c1: C).(\forall (d1: C).((clear c1 d1) \to (\forall (g: G).(\forall 
 (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda 
 (c2: C).(clear c2 d2))))))))
 \def
- \lambda (c1: C).(\lambda (d1: C).(\lambda (H: (clear c1 d1)).(clear_ind 
+ \lambda (c1: C).(\lambda (d1: C).(\lambda (H: (clear c1 d1)).(let TMP_3 \def 
 (\lambda (c: C).(\lambda (c0: C).(\forall (g: G).(\forall (d2: C).((wf3 g c0 
-d2) \to (ex2 C (\lambda (c2: C).(wf3 g c c2)) (\lambda (c2: C).(clear c2 
-d2)))))))) (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(\lambda (g: 
-G).(\lambda (d2: C).(\lambda (H0: (wf3 g (CHead e (Bind b) u) d2)).(let H_x 
-\def (wf3_gen_bind1 g e d2 u b H0) in (let H1 \def H_x in (or_ind (ex3_2 C T 
-(\lambda (c2: C).(\lambda (_: T).(eq C d2 (CHead c2 (Bind b) u)))) (\lambda 
-(c2: C).(\lambda (_: T).(wf3 g e c2))) (\lambda (_: C).(\lambda (w: T).(ty3 g 
-e u w)))) (ex3 C (\lambda (c2: C).(eq C d2 (CHead c2 (Bind Void) (TSort O)))) 
-(\lambda (c2: C).(wf3 g e c2)) (\lambda (_: C).(\forall (w: T).((ty3 g e u w) 
-\to False)))) (ex2 C (\lambda (c2: C).(wf3 g (CHead e (Bind b) u) c2)) 
-(\lambda (c2: C).(clear c2 d2))) (\lambda (H2: (ex3_2 C T (\lambda (c2: 
+d2) \to (let TMP_1 \def (\lambda (c2: C).(wf3 g c c2)) in (let TMP_2 \def 
+(\lambda (c2: C).(clear c2 d2)) in (ex2 C TMP_1 TMP_2)))))))) in (let TMP_87 
+\def (\lambda (b: B).(\lambda (e: C).(\lambda (u: T).(\lambda (g: G).(\lambda 
+(d2: C).(\lambda (H0: (wf3 g (CHead e (Bind b) u) d2)).(let H_x \def 
+(wf3_gen_bind1 g e d2 u b H0) in (let H1 \def H_x in (let TMP_6 \def (\lambda 
+(c2: C).(\lambda (_: T).(let TMP_4 \def (Bind b) in (let TMP_5 \def (CHead c2 
+TMP_4 u) in (eq C d2 TMP_5))))) in (let TMP_7 \def (\lambda (c2: C).(\lambda 
+(_: T).(wf3 g e c2))) in (let TMP_8 \def (\lambda (_: C).(\lambda (w: T).(ty3 
+g e u w))) in (let TMP_9 \def (ex3_2 C T TMP_6 TMP_7 TMP_8) in (let TMP_13 
+\def (\lambda (c2: C).(let TMP_10 \def (Bind Void) in (let TMP_11 \def (TSort 
+O) in (let TMP_12 \def (CHead c2 TMP_10 TMP_11) in (eq C d2 TMP_12))))) in 
+(let TMP_14 \def (\lambda (c2: C).(wf3 g e c2)) in (let TMP_15 \def (\lambda 
+(_: C).(\forall (w: T).((ty3 g e u w) \to False))) in (let TMP_16 \def (ex3 C 
+TMP_13 TMP_14 TMP_15) in (let TMP_19 \def (\lambda (c2: C).(let TMP_17 \def 
+(Bind b) in (let TMP_18 \def (CHead e TMP_17 u) in (wf3 g TMP_18 c2)))) in 
+(let TMP_20 \def (\lambda (c2: C).(clear c2 d2)) in (let TMP_21 \def (ex2 C 
+TMP_19 TMP_20) in (let TMP_51 \def (\lambda (H2: (ex3_2 C T (\lambda (c2: 
 C).(\lambda (_: T).(eq C d2 (CHead c2 (Bind b) u)))) (\lambda (c2: 
 C).(\lambda (_: T).(wf3 g e c2))) (\lambda (_: C).(\lambda (w: T).(ty3 g e u 
-w))))).(ex3_2_ind C T (\lambda (c2: C).(\lambda (_: T).(eq C d2 (CHead c2 
-(Bind b) u)))) (\lambda (c2: C).(\lambda (_: T).(wf3 g e c2))) (\lambda (_: 
-C).(\lambda (w: T).(ty3 g e u w))) (ex2 C (\lambda (c2: C).(wf3 g (CHead e 
-(Bind b) u) c2)) (\lambda (c2: C).(clear c2 d2))) (\lambda (x0: C).(\lambda 
-(x1: T).(\lambda (H3: (eq C d2 (CHead x0 (Bind b) u))).(\lambda (H4: (wf3 g e 
-x0)).(\lambda (H5: (ty3 g e u x1)).(eq_ind_r C (CHead x0 (Bind b) u) (\lambda 
-(c: C).(ex2 C (\lambda (c2: C).(wf3 g (CHead e (Bind b) u) c2)) (\lambda (c2: 
-C).(clear c2 c)))) (ex_intro2 C (\lambda (c2: C).(wf3 g (CHead e (Bind b) u) 
-c2)) (\lambda (c2: C).(clear c2 (CHead x0 (Bind b) u))) (CHead x0 (Bind b) u) 
-(wf3_bind g e x0 H4 u x1 H5 b) (clear_bind b x0 u)) d2 H3)))))) H2)) (\lambda 
-(H2: (ex3 C (\lambda (c2: C).(eq C d2 (CHead c2 (Bind Void) (TSort O)))) 
-(\lambda (c2: C).(wf3 g e c2)) (\lambda (_: C).(\forall (w: T).((ty3 g e u w) 
-\to False))))).(ex3_ind C (\lambda (c2: C).(eq C d2 (CHead c2 (Bind Void) 
-(TSort O)))) (\lambda (c2: C).(wf3 g e c2)) (\lambda (_: C).(\forall (w: 
-T).((ty3 g e u w) \to False))) (ex2 C (\lambda (c2: C).(wf3 g (CHead e (Bind 
-b) u) c2)) (\lambda (c2: C).(clear c2 d2))) (\lambda (x0: C).(\lambda (H3: 
-(eq C d2 (CHead x0 (Bind Void) (TSort O)))).(\lambda (H4: (wf3 g e 
-x0)).(\lambda (H5: ((\forall (w: T).((ty3 g e u w) \to False)))).(eq_ind_r C 
-(CHead x0 (Bind Void) (TSort O)) (\lambda (c: C).(ex2 C (\lambda (c2: C).(wf3 
-g (CHead e (Bind b) u) c2)) (\lambda (c2: C).(clear c2 c)))) (ex_intro2 C 
-(\lambda (c2: C).(wf3 g (CHead e (Bind b) u) c2)) (\lambda (c2: C).(clear c2 
-(CHead x0 (Bind Void) (TSort O)))) (CHead x0 (Bind Void) (TSort O)) (wf3_void 
-g e x0 H4 u H5 b) (clear_bind Void x0 (TSort O))) d2 H3))))) H2)) H1))))))))) 
-(\lambda (e: C).(\lambda (c: C).(\lambda (_: (clear e c)).(\lambda (H1: 
-((\forall (g: G).(\forall (d2: C).((wf3 g c d2) \to (ex2 C (\lambda (c2: 
-C).(wf3 g e c2)) (\lambda (c2: C).(clear c2 d2)))))))).(\lambda (f: 
-F).(\lambda (u: T).(\lambda (g: G).(\lambda (d2: C).(\lambda (H2: (wf3 g c 
-d2)).(let H_x \def (H1 g d2 H2) in (let H3 \def H_x in (ex2_ind C (\lambda 
-(c2: C).(wf3 g e c2)) (\lambda (c2: C).(clear c2 d2)) (ex2 C (\lambda (c2: 
-C).(wf3 g (CHead e (Flat f) u) c2)) (\lambda (c2: C).(clear c2 d2))) (\lambda 
-(x: C).(\lambda (H4: (wf3 g e x)).(\lambda (H5: (clear x d2)).(ex_intro2 C 
-(\lambda (c2: C).(wf3 g (CHead e (Flat f) u) c2)) (\lambda (c2: C).(clear c2 
-d2)) x (wf3_flat g e x H4 u f) H5)))) H3)))))))))))) c1 d1 H))).
-(* COMMENTS
-Initial nodes: 1023
-END *)
+w))))).(let TMP_24 \def (\lambda (c2: C).(\lambda (_: T).(let TMP_22 \def 
+(Bind b) in (let TMP_23 \def (CHead c2 TMP_22 u) in (eq C d2 TMP_23))))) in 
+(let TMP_25 \def (\lambda (c2: C).(\lambda (_: T).(wf3 g e c2))) in (let 
+TMP_26 \def (\lambda (_: C).(\lambda (w: T).(ty3 g e u w))) in (let TMP_29 
+\def (\lambda (c2: C).(let TMP_27 \def (Bind b) in (let TMP_28 \def (CHead e 
+TMP_27 u) in (wf3 g TMP_28 c2)))) in (let TMP_30 \def (\lambda (c2: C).(clear 
+c2 d2)) in (let TMP_31 \def (ex2 C TMP_29 TMP_30) in (let TMP_50 \def 
+(\lambda (x0: C).(\lambda (x1: T).(\lambda (H3: (eq C d2 (CHead x0 (Bind b) 
+u))).(\lambda (H4: (wf3 g e x0)).(\lambda (H5: (ty3 g e u x1)).(let TMP_32 
+\def (Bind b) in (let TMP_33 \def (CHead x0 TMP_32 u) in (let TMP_38 \def 
+(\lambda (c: C).(let TMP_36 \def (\lambda (c2: C).(let TMP_34 \def (Bind b) 
+in (let TMP_35 \def (CHead e TMP_34 u) in (wf3 g TMP_35 c2)))) in (let TMP_37 
+\def (\lambda (c2: C).(clear c2 c)) in (ex2 C TMP_36 TMP_37)))) in (let 
+TMP_41 \def (\lambda (c2: C).(let TMP_39 \def (Bind b) in (let TMP_40 \def 
+(CHead e TMP_39 u) in (wf3 g TMP_40 c2)))) in (let TMP_44 \def (\lambda (c2: 
+C).(let TMP_42 \def (Bind b) in (let TMP_43 \def (CHead x0 TMP_42 u) in 
+(clear c2 TMP_43)))) in (let TMP_45 \def (Bind b) in (let TMP_46 \def (CHead 
+x0 TMP_45 u) in (let TMP_47 \def (wf3_bind g e x0 H4 u x1 H5 b) in (let 
+TMP_48 \def (clear_bind b x0 u) in (let TMP_49 \def (ex_intro2 C TMP_41 
+TMP_44 TMP_46 TMP_47 TMP_48) in (eq_ind_r C TMP_33 TMP_38 TMP_49 d2 
+H3)))))))))))))))) in (ex3_2_ind C T TMP_24 TMP_25 TMP_26 TMP_31 TMP_50 
+H2))))))))) in (let TMP_86 \def (\lambda (H2: (ex3 C (\lambda (c2: C).(eq C 
+d2 (CHead c2 (Bind Void) (TSort O)))) (\lambda (c2: C).(wf3 g e c2)) (\lambda 
+(_: C).(\forall (w: T).((ty3 g e u w) \to False))))).(let TMP_55 \def 
+(\lambda (c2: C).(let TMP_52 \def (Bind Void) in (let TMP_53 \def (TSort O) 
+in (let TMP_54 \def (CHead c2 TMP_52 TMP_53) in (eq C d2 TMP_54))))) in (let 
+TMP_56 \def (\lambda (c2: C).(wf3 g e c2)) in (let TMP_57 \def (\lambda (_: 
+C).(\forall (w: T).((ty3 g e u w) \to False))) in (let TMP_60 \def (\lambda 
+(c2: C).(let TMP_58 \def (Bind b) in (let TMP_59 \def (CHead e TMP_58 u) in 
+(wf3 g TMP_59 c2)))) in (let TMP_61 \def (\lambda (c2: C).(clear c2 d2)) in 
+(let TMP_62 \def (ex2 C TMP_60 TMP_61) in (let TMP_85 \def (\lambda (x0: 
+C).(\lambda (H3: (eq C d2 (CHead x0 (Bind Void) (TSort O)))).(\lambda (H4: 
+(wf3 g e x0)).(\lambda (H5: ((\forall (w: T).((ty3 g e u w) \to 
+False)))).(let TMP_63 \def (Bind Void) in (let TMP_64 \def (TSort O) in (let 
+TMP_65 \def (CHead x0 TMP_63 TMP_64) in (let TMP_70 \def (\lambda (c: C).(let 
+TMP_68 \def (\lambda (c2: C).(let TMP_66 \def (Bind b) in (let TMP_67 \def 
+(CHead e TMP_66 u) in (wf3 g TMP_67 c2)))) in (let TMP_69 \def (\lambda (c2: 
+C).(clear c2 c)) in (ex2 C TMP_68 TMP_69)))) in (let TMP_73 \def (\lambda 
+(c2: C).(let TMP_71 \def (Bind b) in (let TMP_72 \def (CHead e TMP_71 u) in 
+(wf3 g TMP_72 c2)))) in (let TMP_77 \def (\lambda (c2: C).(let TMP_74 \def 
+(Bind Void) in (let TMP_75 \def (TSort O) in (let TMP_76 \def (CHead x0 
+TMP_74 TMP_75) in (clear c2 TMP_76))))) in (let TMP_78 \def (Bind Void) in 
+(let TMP_79 \def (TSort O) in (let TMP_80 \def (CHead x0 TMP_78 TMP_79) in 
+(let TMP_81 \def (wf3_void g e x0 H4 u H5 b) in (let TMP_82 \def (TSort O) in 
+(let TMP_83 \def (clear_bind Void x0 TMP_82) in (let TMP_84 \def (ex_intro2 C 
+TMP_73 TMP_77 TMP_80 TMP_81 TMP_83) in (eq_ind_r C TMP_65 TMP_70 TMP_84 d2 
+H3)))))))))))))))))) in (ex3_ind C TMP_55 TMP_56 TMP_57 TMP_62 TMP_85 
+H2))))))))) in (or_ind TMP_9 TMP_16 TMP_21 TMP_51 TMP_86 
+H1)))))))))))))))))))))) in (let TMP_101 \def (\lambda (e: C).(\lambda (c: 
+C).(\lambda (_: (clear e c)).(\lambda (H1: ((\forall (g: G).(\forall (d2: 
+C).((wf3 g c d2) \to (ex2 C (\lambda (c2: C).(wf3 g e c2)) (\lambda (c2: 
+C).(clear c2 d2)))))))).(\lambda (f: F).(\lambda (u: T).(\lambda (g: 
+G).(\lambda (d2: C).(\lambda (H2: (wf3 g c d2)).(let H_x \def (H1 g d2 H2) in 
+(let H3 \def H_x in (let TMP_88 \def (\lambda (c2: C).(wf3 g e c2)) in (let 
+TMP_89 \def (\lambda (c2: C).(clear c2 d2)) in (let TMP_92 \def (\lambda (c2: 
+C).(let TMP_90 \def (Flat f) in (let TMP_91 \def (CHead e TMP_90 u) in (wf3 g 
+TMP_91 c2)))) in (let TMP_93 \def (\lambda (c2: C).(clear c2 d2)) in (let 
+TMP_94 \def (ex2 C TMP_92 TMP_93) in (let TMP_100 \def (\lambda (x: 
+C).(\lambda (H4: (wf3 g e x)).(\lambda (H5: (clear x d2)).(let TMP_97 \def 
+(\lambda (c2: C).(let TMP_95 \def (Flat f) in (let TMP_96 \def (CHead e 
+TMP_95 u) in (wf3 g TMP_96 c2)))) in (let TMP_98 \def (\lambda (c2: C).(clear 
+c2 d2)) in (let TMP_99 \def (wf3_flat g e x H4 u f) in (ex_intro2 C TMP_97 
+TMP_98 x TMP_99 H5))))))) in (ex2_ind C TMP_88 TMP_89 TMP_94 TMP_100 
+H3)))))))))))))))))) in (clear_ind TMP_3 TMP_87 TMP_101 c1 d1 H)))))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/defs.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/defs.ma
index a99661941aa93f5c4ee9b4124b50a78f3279af1a..df5eedc6c627f13ad03b7eac56f115ecc3d08f80 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/wf3/defs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/defs.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/ty3/defs.ma".
+include "basic_1/ty3/defs.ma".
 
 inductive wf3 (g: G): C \to (C \to Prop) \def
 | wf3_sort: \forall (m: nat).(wf3 g (CSort m) (CSort m))

diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma
index 71c903f0641518006bd77aa72b668fa03d9f7955..62ecb8cc0e5c45111809b4cc716fdff50020b1cf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/fwd.ma
@@ -14,44 +14,71 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/wf3/defs.ma".
+include "basic_1/wf3/defs.ma".
+
+let rec wf3_ind (g: G) (P: (C \to (C \to Prop))) (f: (\forall (m: nat).(P 
+(CSort m) (CSort m)))) (f0: (\forall (c1: C).(\forall (c2: C).((wf3 g c1 c2) 
+\to ((P c1 c2) \to (\forall (u: T).(\forall (t: T).((ty3 g c1 u t) \to 
+(\forall (b: B).(P (CHead c1 (Bind b) u) (CHead c2 (Bind b) u))))))))))) (f1: 
+(\forall (c1: C).(\forall (c2: C).((wf3 g c1 c2) \to ((P c1 c2) \to (\forall 
+(u: T).(((\forall (t: T).((ty3 g c1 u t) \to False))) \to (\forall (b: B).(P 
+(CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O))))))))))) (f2: (\forall 
+(c1: C).(\forall (c2: C).((wf3 g c1 c2) \to ((P c1 c2) \to (\forall (u: 
+T).(\forall (f2: F).(P (CHead c1 (Flat f2) u) c2)))))))) (c: C) (c0: C) (w: 
+wf3 g c c0) on w: P c c0 \def match w with [(wf3_sort m) \Rightarrow (f m) | 
+(wf3_bind c1 c2 w0 u t t0 b) \Rightarrow (let TMP_3 \def ((wf3_ind g P f f0 
+f1 f2) c1 c2 w0) in (f0 c1 c2 w0 TMP_3 u t t0 b)) | (wf3_void c1 c2 w0 u f3 
+b) \Rightarrow (let TMP_2 \def ((wf3_ind g P f f0 f1 f2) c1 c2 w0) in (f1 c1 
+c2 w0 TMP_2 u f3 b)) | (wf3_flat c1 c2 w0 u f3) \Rightarrow (let TMP_1 \def 
+((wf3_ind g P f f0 f1 f2) c1 c2 w0) in (f2 c1 c2 w0 TMP_1 u f3))].
 
 theorem wf3_gen_sort1:
  \forall (g: G).(\forall (x: C).(\forall (m: nat).((wf3 g (CSort m) x) \to 
 (eq C x (CSort m)))))
 \def
  \lambda (g: G).(\lambda (x: C).(\lambda (m: nat).(\lambda (H: (wf3 g (CSort 
-m) x)).(insert_eq C (CSort m) (\lambda (c: C).(wf3 g c x)) (\lambda (c: 
-C).(eq C x c)) (\lambda (y: C).(\lambda (H0: (wf3 g y x)).(wf3_ind g (\lambda 
-(c: C).(\lambda (c0: C).((eq C c (CSort m)) \to (eq C c0 c)))) (\lambda (m0: 
-nat).(\lambda (H1: (eq C (CSort m0) (CSort m))).(let H2 \def (f_equal C nat 
-(\lambda (e: C).(match e in C return (\lambda (_: C).nat) with [(CSort n) 
-\Rightarrow n | (CHead _ _ _) \Rightarrow m0])) (CSort m0) (CSort m) H1) in 
-(eq_ind_r nat m (\lambda (n: nat).(eq C (CSort n) (CSort n))) (refl_equal C 
-(CSort m)) m0 H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (wf3 g c1 
+m) x)).(let TMP_1 \def (CSort m) in (let TMP_2 \def (\lambda (c: C).(wf3 g c 
+x)) in (let TMP_3 \def (\lambda (c: C).(eq C x c)) in (let TMP_43 \def 
+(\lambda (y: C).(\lambda (H0: (wf3 g y x)).(let TMP_4 \def (\lambda (c: 
+C).(\lambda (c0: C).((eq C c (CSort m)) \to (eq C c0 c)))) in (let TMP_13 
+\def (\lambda (m0: nat).(\lambda (H1: (eq C (CSort m0) (CSort m))).(let TMP_5 
+\def (\lambda (e: C).(match e with [(CSort n) \Rightarrow n | (CHead _ _ _) 
+\Rightarrow m0])) in (let TMP_6 \def (CSort m0) in (let TMP_7 \def (CSort m) 
+in (let H2 \def (f_equal C nat TMP_5 TMP_6 TMP_7 H1) in (let TMP_10 \def 
+(\lambda (n: nat).(let TMP_8 \def (CSort n) in (let TMP_9 \def (CSort n) in 
+(eq C TMP_8 TMP_9)))) in (let TMP_11 \def (CSort m) in (let TMP_12 \def 
+(refl_equal C TMP_11) in (eq_ind_r nat m TMP_10 TMP_12 m0 H2)))))))))) in 
+(let TMP_23 \def (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (wf3 g c1 
 c2)).(\lambda (_: (((eq C c1 (CSort m)) \to (eq C c2 c1)))).(\lambda (u: 
 T).(\lambda (t: T).(\lambda (_: (ty3 g c1 u t)).(\lambda (b: B).(\lambda (H4: 
-(eq C (CHead c1 (Bind b) u) (CSort m))).(let H5 \def (eq_ind C (CHead c1 
-(Bind b) u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) with 
-[(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) I (CSort m) 
-H4) in (False_ind (eq C (CHead c2 (Bind b) u) (CHead c1 (Bind b) u)) 
-H5))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (wf3 g c1 
+(eq C (CHead c1 (Bind b) u) (CSort m))).(let TMP_14 \def (Bind b) in (let 
+TMP_15 \def (CHead c1 TMP_14 u) in (let TMP_16 \def (\lambda (ee: C).(match 
+ee with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow True])) in 
+(let TMP_17 \def (CSort m) in (let H5 \def (eq_ind C TMP_15 TMP_16 I TMP_17 
+H4) in (let TMP_18 \def (Bind b) in (let TMP_19 \def (CHead c2 TMP_18 u) in 
+(let TMP_20 \def (Bind b) in (let TMP_21 \def (CHead c1 TMP_20 u) in (let 
+TMP_22 \def (eq C TMP_19 TMP_21) in (False_ind TMP_22 H5)))))))))))))))))))) 
+in (let TMP_34 \def (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (wf3 g c1 
 c2)).(\lambda (_: (((eq C c1 (CSort m)) \to (eq C c2 c1)))).(\lambda (u: 
 T).(\lambda (_: ((\forall (t: T).((ty3 g c1 u t) \to False)))).(\lambda (b: 
-B).(\lambda (H4: (eq C (CHead c1 (Bind b) u) (CSort m))).(let H5 \def (eq_ind 
-C (CHead c1 (Bind b) u) (\lambda (ee: C).(match ee in C return (\lambda (_: 
-C).Prop) with [(CSort _) \Rightarrow False | (CHead _ _ _) \Rightarrow 
-True])) I (CSort m) H4) in (False_ind (eq C (CHead c2 (Bind Void) (TSort O)) 
-(CHead c1 (Bind b) u)) H5)))))))))) (\lambda (c1: C).(\lambda (c2: 
-C).(\lambda (_: (wf3 g c1 c2)).(\lambda (_: (((eq C c1 (CSort m)) \to (eq C 
-c2 c1)))).(\lambda (u: T).(\lambda (f: F).(\lambda (H3: (eq C (CHead c1 (Flat 
-f) u) (CSort m))).(let H4 \def (eq_ind C (CHead c1 (Flat f) u) (\lambda (ee: 
-C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow 
-False | (CHead _ _ _) \Rightarrow True])) I (CSort m) H3) in (False_ind (eq C 
-c2 (CHead c1 (Flat f) u)) H4))))))))) y x H0))) H)))).
-(* COMMENTS
-Initial nodes: 523
-END *)
+B).(\lambda (H4: (eq C (CHead c1 (Bind b) u) (CSort m))).(let TMP_24 \def 
+(Bind b) in (let TMP_25 \def (CHead c1 TMP_24 u) in (let TMP_26 \def (\lambda 
+(ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ _ _) 
+\Rightarrow True])) in (let TMP_27 \def (CSort m) in (let H5 \def (eq_ind C 
+TMP_25 TMP_26 I TMP_27 H4) in (let TMP_28 \def (Bind Void) in (let TMP_29 
+\def (TSort O) in (let TMP_30 \def (CHead c2 TMP_28 TMP_29) in (let TMP_31 
+\def (Bind b) in (let TMP_32 \def (CHead c1 TMP_31 u) in (let TMP_33 \def (eq 
+C TMP_30 TMP_32) in (False_ind TMP_33 H5)))))))))))))))))))) in (let TMP_42 
+\def (\lambda (c1: C).(\lambda (c2: C).(\lambda (_: (wf3 g c1 c2)).(\lambda 
+(_: (((eq C c1 (CSort m)) \to (eq C c2 c1)))).(\lambda (u: T).(\lambda (f: 
+F).(\lambda (H3: (eq C (CHead c1 (Flat f) u) (CSort m))).(let TMP_35 \def 
+(Flat f) in (let TMP_36 \def (CHead c1 TMP_35 u) in (let TMP_37 \def (\lambda 
+(ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ _ _) 
+\Rightarrow True])) in (let TMP_38 \def (CSort m) in (let H4 \def (eq_ind C 
+TMP_36 TMP_37 I TMP_38 H3) in (let TMP_39 \def (Flat f) in (let TMP_40 \def 
+(CHead c1 TMP_39 u) in (let TMP_41 \def (eq C c2 TMP_40) in (False_ind TMP_41 
+H4)))))))))))))))) in (wf3_ind g TMP_4 TMP_13 TMP_23 TMP_34 TMP_42 y x 
+H0)))))))) in (insert_eq C TMP_1 TMP_2 TMP_3 TMP_43 H)))))))).
 
 theorem wf3_gen_bind1:
  \forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (b: 
@@ -63,249 +90,509 @@ C).(wf3 g c1 c2)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to
 False))))))))))
 \def
  \lambda (g: G).(\lambda (c1: C).(\lambda (x: C).(\lambda (v: T).(\lambda (b: 
-B).(\lambda (H: (wf3 g (CHead c1 (Bind b) v) x)).(insert_eq C (CHead c1 (Bind 
-b) v) (\lambda (c: C).(wf3 g c x)) (\lambda (_: C).(or (ex3_2 C T (\lambda 
-(c2: C).(\lambda (_: T).(eq C x (CHead c2 (Bind b) v)))) (\lambda (c2: 
-C).(\lambda (_: T).(wf3 g c1 c2))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 
-v w)))) (ex3 C (\lambda (c2: C).(eq C x (CHead c2 (Bind Void) (TSort O)))) 
-(\lambda (c2: C).(wf3 g c1 c2)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v 
-w) \to False)))))) (\lambda (y: C).(\lambda (H0: (wf3 g y x)).(wf3_ind g 
-(\lambda (c: C).(\lambda (c0: C).((eq C c (CHead c1 (Bind b) v)) \to (or 
-(ex3_2 C T (\lambda (c2: C).(\lambda (_: T).(eq C c0 (CHead c2 (Bind b) v)))) 
-(\lambda (c2: C).(\lambda (_: T).(wf3 g c1 c2))) (\lambda (_: C).(\lambda (w: 
-T).(ty3 g c1 v w)))) (ex3 C (\lambda (c2: C).(eq C c0 (CHead c2 (Bind Void) 
-(TSort O)))) (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (_: C).(\forall (w: 
-T).((ty3 g c1 v w) \to False)))))))) (\lambda (m: nat).(\lambda (H1: (eq C 
-(CSort m) (CHead c1 (Bind b) v))).(let H2 \def (eq_ind C (CSort m) (\lambda 
-(ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) 
-\Rightarrow True | (CHead _ _ _) \Rightarrow False])) I (CHead c1 (Bind b) v) 
-H1) in (False_ind (or (ex3_2 C T (\lambda (c2: C).(\lambda (_: T).(eq C 
-(CSort m) (CHead c2 (Bind b) v)))) (\lambda (c2: C).(\lambda (_: T).(wf3 g c1 
-c2))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda (c2: 
-C).(eq C (CSort m) (CHead c2 (Bind Void) (TSort O)))) (\lambda (c2: C).(wf3 g 
-c1 c2)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False))))) H2)))) 
-(\lambda (c0: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: 
-(((eq C c0 (CHead c1 (Bind b) v)) \to (or (ex3_2 C T (\lambda (c3: 
-C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: 
-C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 
-v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) 
-(\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v 
-w) \to False)))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H3: (ty3 g c0 
-u t)).(\lambda (b0: B).(\lambda (H4: (eq C (CHead c0 (Bind b0) u) (CHead c1 
-(Bind b) v))).(let H5 \def (f_equal C C (\lambda (e: C).(match e in C return 
-(\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow 
-c])) (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v) H4) in ((let H6 \def 
-(f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with 
-[(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k in K return 
-(\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow 
-b0])])) (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v) H4) in ((let H7 \def 
-(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with 
-[(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead c0 (Bind 
-b0) u) (CHead c1 (Bind b) v) H4) in (\lambda (H8: (eq B b0 b)).(\lambda (H9: 
-(eq C c0 c1)).(eq_ind_r B b (\lambda (b1: B).(or (ex3_2 C T (\lambda (c3: 
-C).(\lambda (_: T).(eq C (CHead c2 (Bind b1) u) (CHead c3 (Bind b) v)))) 
-(\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: 
-T).(ty3 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C (CHead c2 (Bind b1) u) 
-(CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda 
-(_: C).(\forall (w: T).((ty3 g c1 v w) \to False)))))) (let H10 \def (eq_ind 
-T u (\lambda (t0: T).(ty3 g c0 t0 t)) H3 v H7) in (eq_ind_r T v (\lambda (t0: 
-T).(or (ex3_2 C T (\lambda (c3: C).(\lambda (_: T).(eq C (CHead c2 (Bind b) 
-t0) (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) 
-(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq 
-C (CHead c2 (Bind b) t0) (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: 
-C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to 
-False)))))) (let H11 \def (eq_ind C c0 (\lambda (c: C).(ty3 g c v t)) H10 c1 
-H9) in (let H12 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead c1 (Bind b) 
-v)) \to (or (ex3_2 C T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 
-(Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: 
-C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead 
-c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: 
-C).(\forall (w: T).((ty3 g c1 v w) \to False))))))) H2 c1 H9) in (let H13 
-\def (eq_ind C c0 (\lambda (c: C).(wf3 g c c2)) H1 c1 H9) in (or_introl 
-(ex3_2 C T (\lambda (c3: C).(\lambda (_: T).(eq C (CHead c2 (Bind b) v) 
-(CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) 
-(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq 
-C (CHead c2 (Bind b) v) (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: 
-C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to 
-False)))) (ex3_2_intro C T (\lambda (c3: C).(\lambda (_: T).(eq C (CHead c2 
-(Bind b) v) (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g 
-c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) c2 t (refl_equal C 
-(CHead c2 (Bind b) v)) H13 H11))))) u H7)) b0 H8)))) H6)) H5))))))))))) 
-(\lambda (c0: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: 
-(((eq C c0 (CHead c1 (Bind b) v)) \to (or (ex3_2 C T (\lambda (c3: 
-C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: 
-C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 
-v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) 
-(\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v 
-w) \to False)))))))).(\lambda (u: T).(\lambda (H3: ((\forall (t: T).((ty3 g 
-c0 u t) \to False)))).(\lambda (b0: B).(\lambda (H4: (eq C (CHead c0 (Bind 
-b0) u) (CHead c1 (Bind b) v))).(let H5 \def (f_equal C C (\lambda (e: 
-C).(match e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c0 | 
-(CHead c _ _) \Rightarrow c])) (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v) 
-H4) in ((let H6 \def (f_equal C B (\lambda (e: C).(match e in C return 
-(\lambda (_: C).B) with [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow 
-(match k in K return (\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | 
-(Flat _) \Rightarrow b0])])) (CHead c0 (Bind b0) u) (CHead c1 (Bind b) v) H4) 
-in ((let H7 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda 
-(_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) 
-(CHead c0 (Bind b0) u) (CHead c1 (Bind b) v) H4) in (\lambda (_: (eq B b0 
-b)).(\lambda (H9: (eq C c0 c1)).(let H10 \def (eq_ind T u (\lambda (t: 
-T).(\forall (t0: T).((ty3 g c0 t t0) \to False))) H3 v H7) in (let H11 \def 
-(eq_ind C c0 (\lambda (c: C).(\forall (t: T).((ty3 g c v t) \to False))) H10 
-c1 H9) in (let H12 \def (eq_ind C c0 (\lambda (c: C).((eq C c (CHead c1 (Bind 
+B).(\lambda (H: (wf3 g (CHead c1 (Bind b) v) x)).(let TMP_1 \def (Bind b) in 
+(let TMP_2 \def (CHead c1 TMP_1 v) in (let TMP_3 \def (\lambda (c: C).(wf3 g 
+c x)) in (let TMP_17 \def (\lambda (_: C).(let TMP_6 \def (\lambda (c2: 
+C).(\lambda (_: T).(let TMP_4 \def (Bind b) in (let TMP_5 \def (CHead c2 
+TMP_4 v) in (eq C x TMP_5))))) in (let TMP_7 \def (\lambda (c2: C).(\lambda 
+(_: T).(wf3 g c1 c2))) in (let TMP_8 \def (\lambda (_: C).(\lambda (w: 
+T).(ty3 g c1 v w))) in (let TMP_9 \def (ex3_2 C T TMP_6 TMP_7 TMP_8) in (let 
+TMP_13 \def (\lambda (c2: C).(let TMP_10 \def (Bind Void) in (let TMP_11 \def 
+(TSort O) in (let TMP_12 \def (CHead c2 TMP_10 TMP_11) in (eq C x TMP_12))))) 
+in (let TMP_14 \def (\lambda (c2: C).(wf3 g c1 c2)) in (let TMP_15 \def 
+(\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_16 
+\def (ex3 C TMP_13 TMP_14 TMP_15) in (or TMP_9 TMP_16)))))))))) in (let 
+TMP_242 \def (\lambda (y: C).(\lambda (H0: (wf3 g y x)).(let TMP_31 \def 
+(\lambda (c: C).(\lambda (c0: C).((eq C c (CHead c1 (Bind b) v)) \to (let 
+TMP_20 \def (\lambda (c2: C).(\lambda (_: T).(let TMP_18 \def (Bind b) in 
+(let TMP_19 \def (CHead c2 TMP_18 v) in (eq C c0 TMP_19))))) in (let TMP_21 
+\def (\lambda (c2: C).(\lambda (_: T).(wf3 g c1 c2))) in (let TMP_22 \def 
+(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_23 \def (ex3_2 C 
+T TMP_20 TMP_21 TMP_22) in (let TMP_27 \def (\lambda (c2: C).(let TMP_24 \def 
+(Bind Void) in (let TMP_25 \def (TSort O) in (let TMP_26 \def (CHead c2 
+TMP_24 TMP_25) in (eq C c0 TMP_26))))) in (let TMP_28 \def (\lambda (c2: 
+C).(wf3 g c1 c2)) in (let TMP_29 \def (\lambda (_: C).(\forall (w: T).((ty3 g 
+c1 v w) \to False))) in (let TMP_30 \def (ex3 C TMP_27 TMP_28 TMP_29) in (or 
+TMP_23 TMP_30)))))))))))) in (let TMP_52 \def (\lambda (m: nat).(\lambda (H1: 
+(eq C (CSort m) (CHead c1 (Bind b) v))).(let TMP_32 \def (CSort m) in (let 
+TMP_33 \def (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow True | 
+(CHead _ _ _) \Rightarrow False])) in (let TMP_34 \def (Bind b) in (let 
+TMP_35 \def (CHead c1 TMP_34 v) in (let H2 \def (eq_ind C TMP_32 TMP_33 I 
+TMP_35 H1) in (let TMP_39 \def (\lambda (c2: C).(\lambda (_: T).(let TMP_36 
+\def (CSort m) in (let TMP_37 \def (Bind b) in (let TMP_38 \def (CHead c2 
+TMP_37 v) in (eq C TMP_36 TMP_38)))))) in (let TMP_40 \def (\lambda (c2: 
+C).(\lambda (_: T).(wf3 g c1 c2))) in (let TMP_41 \def (\lambda (_: 
+C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_42 \def (ex3_2 C T TMP_39 
+TMP_40 TMP_41) in (let TMP_47 \def (\lambda (c2: C).(let TMP_43 \def (CSort 
+m) in (let TMP_44 \def (Bind Void) in (let TMP_45 \def (TSort O) in (let 
+TMP_46 \def (CHead c2 TMP_44 TMP_45) in (eq C TMP_43 TMP_46)))))) in (let 
+TMP_48 \def (\lambda (c2: C).(wf3 g c1 c2)) in (let TMP_49 \def (\lambda (_: 
+C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_50 \def (ex3 C 
+TMP_47 TMP_48 TMP_49) in (let TMP_51 \def (or TMP_42 TMP_50) in (False_ind 
+TMP_51 H2))))))))))))))))) in (let TMP_153 \def (\lambda (c0: C).(\lambda 
+(c2: C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: (((eq C c0 (CHead c1 (Bind 
 b) v)) \to (or (ex3_2 C T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 
 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: 
 C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead 
 c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: 
-C).(\forall (w: T).((ty3 g c1 v w) \to False))))))) H2 c1 H9) in (let H13 
-\def (eq_ind C c0 (\lambda (c: C).(wf3 g c c2)) H1 c1 H9) in (or_intror 
-(ex3_2 C T (\lambda (c3: C).(\lambda (_: T).(eq C (CHead c2 (Bind Void) 
-(TSort O)) (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g 
+C).(\forall (w: T).((ty3 g c1 v w) \to False)))))))).(\lambda (u: T).(\lambda 
+(t: T).(\lambda (H3: (ty3 g c0 u t)).(\lambda (b0: B).(\lambda (H4: (eq C 
+(CHead c0 (Bind b0) u) (CHead c1 (Bind b) v))).(let TMP_53 \def (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) 
+in (let TMP_54 \def (Bind b0) in (let TMP_55 \def (CHead c0 TMP_54 u) in (let 
+TMP_56 \def (Bind b) in (let TMP_57 \def (CHead c1 TMP_56 v) in (let H5 \def 
+(f_equal C C TMP_53 TMP_55 TMP_57 H4) in (let TMP_58 \def (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match 
+k with [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b0])])) in (let 
+TMP_59 \def (Bind b0) in (let TMP_60 \def (CHead c0 TMP_59 u) in (let TMP_61 
+\def (Bind b) in (let TMP_62 \def (CHead c1 TMP_61 v) in (let H6 \def 
+(f_equal C B TMP_58 TMP_60 TMP_62 H4) in (let TMP_63 \def (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) 
+in (let TMP_64 \def (Bind b0) in (let TMP_65 \def (CHead c0 TMP_64 u) in (let 
+TMP_66 \def (Bind b) in (let TMP_67 \def (CHead c1 TMP_66 v) in (let H7 \def 
+(f_equal C T TMP_63 TMP_65 TMP_67 H4) in (let TMP_151 \def (\lambda (H8: (eq 
+B b0 b)).(\lambda (H9: (eq C c0 c1)).(let TMP_85 \def (\lambda (b1: B).(let 
+TMP_72 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_68 \def (Bind b1) in 
+(let TMP_69 \def (CHead c2 TMP_68 u) in (let TMP_70 \def (Bind b) in (let 
+TMP_71 \def (CHead c3 TMP_70 v) in (eq C TMP_69 TMP_71))))))) in (let TMP_73 
+\def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_74 \def 
+(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_75 \def (ex3_2 C 
+T TMP_72 TMP_73 TMP_74) in (let TMP_81 \def (\lambda (c3: C).(let TMP_76 \def 
+(Bind b1) in (let TMP_77 \def (CHead c2 TMP_76 u) in (let TMP_78 \def (Bind 
+Void) in (let TMP_79 \def (TSort O) in (let TMP_80 \def (CHead c3 TMP_78 
+TMP_79) in (eq C TMP_77 TMP_80))))))) in (let TMP_82 \def (\lambda (c3: 
+C).(wf3 g c1 c3)) in (let TMP_83 \def (\lambda (_: C).(\forall (w: T).((ty3 g 
+c1 v w) \to False))) in (let TMP_84 \def (ex3 C TMP_81 TMP_82 TMP_83) in (or 
+TMP_75 TMP_84)))))))))) in (let TMP_86 \def (\lambda (t0: T).(ty3 g c0 t0 t)) 
+in (let H10 \def (eq_ind T u TMP_86 H3 v H7) in (let TMP_104 \def (\lambda 
+(t0: T).(let TMP_91 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_87 \def 
+(Bind b) in (let TMP_88 \def (CHead c2 TMP_87 t0) in (let TMP_89 \def (Bind 
+b) in (let TMP_90 \def (CHead c3 TMP_89 v) in (eq C TMP_88 TMP_90))))))) in 
+(let TMP_92 \def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let 
+TMP_93 \def (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_94 
+\def (ex3_2 C T TMP_91 TMP_92 TMP_93) in (let TMP_100 \def (\lambda (c3: 
+C).(let TMP_95 \def (Bind b) in (let TMP_96 \def (CHead c2 TMP_95 t0) in (let 
+TMP_97 \def (Bind Void) in (let TMP_98 \def (TSort O) in (let TMP_99 \def 
+(CHead c3 TMP_97 TMP_98) in (eq C TMP_96 TMP_99))))))) in (let TMP_101 \def 
+(\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_102 \def (\lambda (_: C).(\forall 
+(w: T).((ty3 g c1 v w) \to False))) in (let TMP_103 \def (ex3 C TMP_100 
+TMP_101 TMP_102) in (or TMP_94 TMP_103)))))))))) in (let TMP_105 \def 
+(\lambda (c: C).(ty3 g c v t)) in (let H11 \def (eq_ind C c0 TMP_105 H10 c1 
+H9) in (let TMP_119 \def (\lambda (c: C).((eq C c (CHead c1 (Bind b) v)) \to 
+(let TMP_108 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_106 \def (Bind b) 
+in (let TMP_107 \def (CHead c3 TMP_106 v) in (eq C c2 TMP_107))))) in (let 
+TMP_109 \def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_110 
+\def (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_111 \def 
+(ex3_2 C T TMP_108 TMP_109 TMP_110) in (let TMP_115 \def (\lambda (c3: 
+C).(let TMP_112 \def (Bind Void) in (let TMP_113 \def (TSort O) in (let 
+TMP_114 \def (CHead c3 TMP_112 TMP_113) in (eq C c2 TMP_114))))) in (let 
+TMP_116 \def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_117 \def (\lambda 
+(_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_118 \def (ex3 
+C TMP_115 TMP_116 TMP_117) in (or TMP_111 TMP_118))))))))))) in (let H12 \def 
+(eq_ind C c0 TMP_119 H2 c1 H9) in (let TMP_120 \def (\lambda (c: C).(wf3 g c 
+c2)) in (let H13 \def (eq_ind C c0 TMP_120 H1 c1 H9) in (let TMP_125 \def 
+(\lambda (c3: C).(\lambda (_: T).(let TMP_121 \def (Bind b) in (let TMP_122 
+\def (CHead c2 TMP_121 v) in (let TMP_123 \def (Bind b) in (let TMP_124 \def 
+(CHead c3 TMP_123 v) in (eq C TMP_122 TMP_124))))))) in (let TMP_126 \def 
+(\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_127 \def 
+(\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_128 \def (ex3_2 
+C T TMP_125 TMP_126 TMP_127) in (let TMP_134 \def (\lambda (c3: C).(let 
+TMP_129 \def (Bind b) in (let TMP_130 \def (CHead c2 TMP_129 v) in (let 
+TMP_131 \def (Bind Void) in (let TMP_132 \def (TSort O) in (let TMP_133 \def 
+(CHead c3 TMP_131 TMP_132) in (eq C TMP_130 TMP_133))))))) in (let TMP_135 
+\def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_136 \def (\lambda (_: 
+C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_137 \def (ex3 C 
+TMP_134 TMP_135 TMP_136) in (let TMP_142 \def (\lambda (c3: C).(\lambda (_: 
+T).(let TMP_138 \def (Bind b) in (let TMP_139 \def (CHead c2 TMP_138 v) in 
+(let TMP_140 \def (Bind b) in (let TMP_141 \def (CHead c3 TMP_140 v) in (eq C 
+TMP_139 TMP_141))))))) in (let TMP_143 \def (\lambda (c3: C).(\lambda (_: 
+T).(wf3 g c1 c3))) in (let TMP_144 \def (\lambda (_: C).(\lambda (w: T).(ty3 
+g c1 v w))) in (let TMP_145 \def (Bind b) in (let TMP_146 \def (CHead c2 
+TMP_145 v) in (let TMP_147 \def (refl_equal C TMP_146) in (let TMP_148 \def 
+(ex3_2_intro C T TMP_142 TMP_143 TMP_144 c2 t TMP_147 H13 H11) in (let 
+TMP_149 \def (or_introl TMP_128 TMP_137 TMP_148) in (let TMP_150 \def 
+(eq_ind_r T v TMP_104 TMP_149 u H7) in (eq_ind_r B b TMP_85 TMP_150 b0 
+H8)))))))))))))))))))))))))))))) in (let TMP_152 \def (TMP_151 H6) in 
+(TMP_152 H5)))))))))))))))))))))))))))))) in (let TMP_221 \def (\lambda (c0: 
+C).(\lambda (c2: C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: (((eq C c0 
+(CHead c1 (Bind b) v)) \to (or (ex3_2 C T (\lambda (c3: C).(\lambda (_: 
+T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g 
 c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w)))) (ex3 C (\lambda 
-(c3: C).(eq C (CHead c2 (Bind Void) (TSort O)) (CHead c3 (Bind Void) (TSort 
-O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g 
-c1 v w) \to False)))) (ex3_intro C (\lambda (c3: C).(eq C (CHead c2 (Bind 
-Void) (TSort O)) (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g 
-c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) c2 
-(refl_equal C (CHead c2 (Bind Void) (TSort O))) H13 H11))))))))) H6)) 
-H5)))))))))) (\lambda (c0: C).(\lambda (c2: C).(\lambda (_: (wf3 g c0 
+(c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g 
+c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to 
+False)))))))).(\lambda (u: T).(\lambda (H3: ((\forall (t: T).((ty3 g c0 u t) 
+\to False)))).(\lambda (b0: B).(\lambda (H4: (eq C (CHead c0 (Bind b0) u) 
+(CHead c1 (Bind b) v))).(let TMP_154 \def (\lambda (e: C).(match e with 
+[(CSort _) \Rightarrow c0 | (CHead c _ _) \Rightarrow c])) in (let TMP_155 
+\def (Bind b0) in (let TMP_156 \def (CHead c0 TMP_155 u) in (let TMP_157 \def 
+(Bind b) in (let TMP_158 \def (CHead c1 TMP_157 v) in (let H5 \def (f_equal C 
+C TMP_154 TMP_156 TMP_158 H4) in (let TMP_159 \def (\lambda (e: C).(match e 
+with [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k with 
+[(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b0])])) in (let TMP_160 \def 
+(Bind b0) in (let TMP_161 \def (CHead c0 TMP_160 u) in (let TMP_162 \def 
+(Bind b) in (let TMP_163 \def (CHead c1 TMP_162 v) in (let H6 \def (f_equal C 
+B TMP_159 TMP_161 TMP_163 H4) in (let TMP_164 \def (\lambda (e: C).(match e 
+with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) in (let 
+TMP_165 \def (Bind b0) in (let TMP_166 \def (CHead c0 TMP_165 u) in (let 
+TMP_167 \def (Bind b) in (let TMP_168 \def (CHead c1 TMP_167 v) in (let H7 
+\def (f_equal C T TMP_164 TMP_166 TMP_168 H4) in (let TMP_219 \def (\lambda 
+(_: (eq B b0 b)).(\lambda (H9: (eq C c0 c1)).(let TMP_169 \def (\lambda (t: 
+T).(\forall (t0: T).((ty3 g c0 t t0) \to False))) in (let H10 \def (eq_ind T 
+u TMP_169 H3 v H7) in (let TMP_170 \def (\lambda (c: C).(\forall (t: T).((ty3 
+g c v t) \to False))) in (let H11 \def (eq_ind C c0 TMP_170 H10 c1 H9) in 
+(let TMP_184 \def (\lambda (c: C).((eq C c (CHead c1 (Bind b) v)) \to (let 
+TMP_173 \def (\lambda (c3: C).(\lambda (_: T).(let TMP_171 \def (Bind b) in 
+(let TMP_172 \def (CHead c3 TMP_171 v) in (eq C c2 TMP_172))))) in (let 
+TMP_174 \def (\lambda (c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_175 
+\def (\lambda (_: C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_176 \def 
+(ex3_2 C T TMP_173 TMP_174 TMP_175) in (let TMP_180 \def (\lambda (c3: 
+C).(let TMP_177 \def (Bind Void) in (let TMP_178 \def (TSort O) in (let 
+TMP_179 \def (CHead c3 TMP_177 TMP_178) in (eq C c2 TMP_179))))) in (let 
+TMP_181 \def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_182 \def (\lambda 
+(_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_183 \def (ex3 
+C TMP_180 TMP_181 TMP_182) in (or TMP_176 TMP_183))))))))))) in (let H12 \def 
+(eq_ind C c0 TMP_184 H2 c1 H9) in (let TMP_185 \def (\lambda (c: C).(wf3 g c 
+c2)) in (let H13 \def (eq_ind C c0 TMP_185 H1 c1 H9) in (let TMP_191 \def 
+(\lambda (c3: C).(\lambda (_: T).(let TMP_186 \def (Bind Void) in (let 
+TMP_187 \def (TSort O) in (let TMP_188 \def (CHead c2 TMP_186 TMP_187) in 
+(let TMP_189 \def (Bind b) in (let TMP_190 \def (CHead c3 TMP_189 v) in (eq C 
+TMP_188 TMP_190)))))))) in (let TMP_192 \def (\lambda (c3: C).(\lambda (_: 
+T).(wf3 g c1 c3))) in (let TMP_193 \def (\lambda (_: C).(\lambda (w: T).(ty3 
+g c1 v w))) in (let TMP_194 \def (ex3_2 C T TMP_191 TMP_192 TMP_193) in (let 
+TMP_201 \def (\lambda (c3: C).(let TMP_195 \def (Bind Void) in (let TMP_196 
+\def (TSort O) in (let TMP_197 \def (CHead c2 TMP_195 TMP_196) in (let 
+TMP_198 \def (Bind Void) in (let TMP_199 \def (TSort O) in (let TMP_200 \def 
+(CHead c3 TMP_198 TMP_199) in (eq C TMP_197 TMP_200)))))))) in (let TMP_202 
+\def (\lambda (c3: C).(wf3 g c1 c3)) in (let TMP_203 \def (\lambda (_: 
+C).(\forall (w: T).((ty3 g c1 v w) \to False))) in (let TMP_204 \def (ex3 C 
+TMP_201 TMP_202 TMP_203) in (let TMP_211 \def (\lambda (c3: C).(let TMP_205 
+\def (Bind Void) in (let TMP_206 \def (TSort O) in (let TMP_207 \def (CHead 
+c2 TMP_205 TMP_206) in (let TMP_208 \def (Bind Void) in (let TMP_209 \def 
+(TSort O) in (let TMP_210 \def (CHead c3 TMP_208 TMP_209) in (eq C TMP_207 
+TMP_210)))))))) in (let TMP_212 \def (\lambda (c3: C).(wf3 g c1 c3)) in (let 
+TMP_213 \def (\lambda (_: C).(\forall (w: T).((ty3 g c1 v w) \to False))) in 
+(let TMP_214 \def (Bind Void) in (let TMP_215 \def (TSort O) in (let TMP_216 
+\def (CHead c2 TMP_214 TMP_215) in (let TMP_217 \def (refl_equal C TMP_216) 
+in (let TMP_218 \def (ex3_intro C TMP_211 TMP_212 TMP_213 c2 TMP_217 H13 H11) 
+in (or_intror TMP_194 TMP_204 TMP_218))))))))))))))))))))))))))) in (let 
+TMP_220 \def (TMP_219 H6) in (TMP_220 H5))))))))))))))))))))))))))))) in (let 
+TMP_241 \def (\lambda (c0: C).(\lambda (c2: C).(\lambda (_: (wf3 g c0 
 c2)).(\lambda (_: (((eq C c0 (CHead c1 (Bind b) v)) \to (or (ex3_2 C T 
 (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda 
 (c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 
 g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort 
 O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g 
 c1 v w) \to False)))))))).(\lambda (u: T).(\lambda (f: F).(\lambda (H3: (eq C 
-(CHead c0 (Flat f) u) (CHead c1 (Bind b) v))).(let H4 \def (eq_ind C (CHead 
-c0 (Flat f) u) (\lambda (ee: C).(match ee in C return (\lambda (_: C).Prop) 
-with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k in K 
-return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) 
-\Rightarrow True])])) I (CHead c1 (Bind b) v) H3) in (False_ind (or (ex3_2 C 
-T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda 
-(c3: C).(\lambda (_: T).(wf3 g c1 c3))) (\lambda (_: C).(\lambda (w: T).(ty3 
-g c1 v w)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort 
-O)))) (\lambda (c3: C).(wf3 g c1 c3)) (\lambda (_: C).(\forall (w: T).((ty3 g 
-c1 v w) \to False))))) H4))))))))) y x H0))) H)))))).
-(* COMMENTS
-Initial nodes: 2507
-END *)
+(CHead c0 (Flat f) u) (CHead c1 (Bind b) v))).(let TMP_222 \def (Flat f) in 
+(let TMP_223 \def (CHead c0 TMP_222 u) in (let TMP_224 \def (\lambda (ee: 
+C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow 
+(match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) in 
+(let TMP_225 \def (Bind b) in (let TMP_226 \def (CHead c1 TMP_225 v) in (let 
+H4 \def (eq_ind C TMP_223 TMP_224 I TMP_226 H3) in (let TMP_229 \def (\lambda 
+(c3: C).(\lambda (_: T).(let TMP_227 \def (Bind b) in (let TMP_228 \def 
+(CHead c3 TMP_227 v) in (eq C c2 TMP_228))))) in (let TMP_230 \def (\lambda 
+(c3: C).(\lambda (_: T).(wf3 g c1 c3))) in (let TMP_231 \def (\lambda (_: 
+C).(\lambda (w: T).(ty3 g c1 v w))) in (let TMP_232 \def (ex3_2 C T TMP_229 
+TMP_230 TMP_231) in (let TMP_236 \def (\lambda (c3: C).(let TMP_233 \def 
+(Bind Void) in (let TMP_234 \def (TSort O) in (let TMP_235 \def (CHead c3 
+TMP_233 TMP_234) in (eq C c2 TMP_235))))) in (let TMP_237 \def (\lambda (c3: 
+C).(wf3 g c1 c3)) in (let TMP_238 \def (\lambda (_: C).(\forall (w: T).((ty3 
+g c1 v w) \to False))) in (let TMP_239 \def (ex3 C TMP_236 TMP_237 TMP_238) 
+in (let TMP_240 \def (or TMP_232 TMP_239) in (False_ind TMP_240 
+H4))))))))))))))))))))))) in (wf3_ind g TMP_31 TMP_52 TMP_153 TMP_221 TMP_241 
+y x H0)))))))) in (insert_eq C TMP_2 TMP_3 TMP_17 TMP_242 H))))))))))).
 
 theorem wf3_gen_flat1:
  \forall (g: G).(\forall (c1: C).(\forall (x: C).(\forall (v: T).(\forall (f: 
 F).((wf3 g (CHead c1 (Flat f) v) x) \to (wf3 g c1 x))))))
 \def
  \lambda (g: G).(\lambda (c1: C).(\lambda (x: C).(\lambda (v: T).(\lambda (f: 
-F).(\lambda (H: (wf3 g (CHead c1 (Flat f) v) x)).(insert_eq C (CHead c1 (Flat 
-f) v) (\lambda (c: C).(wf3 g c x)) (\lambda (_: C).(wf3 g c1 x)) (\lambda (y: 
-C).(\lambda (H0: (wf3 g y x)).(wf3_ind g (\lambda (c: C).(\lambda (c0: 
-C).((eq C c (CHead c1 (Flat f) v)) \to (wf3 g c1 c0)))) (\lambda (m: 
-nat).(\lambda (H1: (eq C (CSort m) (CHead c1 (Flat f) v))).(let H2 \def 
-(eq_ind C (CSort m) (\lambda (ee: C).(match ee in C return (\lambda (_: 
-C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow 
-False])) I (CHead c1 (Flat f) v) H1) in (False_ind (wf3 g c1 (CSort m)) 
-H2)))) (\lambda (c0: C).(\lambda (c2: C).(\lambda (_: (wf3 g c0 c2)).(\lambda 
-(_: (((eq C c0 (CHead c1 (Flat f) v)) \to (wf3 g c1 c2)))).(\lambda (u: 
-T).(\lambda (t: T).(\lambda (_: (ty3 g c0 u t)).(\lambda (b: B).(\lambda (H4: 
-(eq C (CHead c0 (Bind b) u) (CHead c1 (Flat f) v))).(let H5 \def (eq_ind C 
-(CHead c0 (Bind b) u) (\lambda (ee: C).(match ee in C return (\lambda (_: 
-C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match 
-k in K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat 
-_) \Rightarrow False])])) I (CHead c1 (Flat f) v) H4) in (False_ind (wf3 g c1 
-(CHead c2 (Bind b) u)) H5))))))))))) (\lambda (c0: C).(\lambda (c2: 
-C).(\lambda (_: (wf3 g c0 c2)).(\lambda (_: (((eq C c0 (CHead c1 (Flat f) v)) 
-\to (wf3 g c1 c2)))).(\lambda (u: T).(\lambda (_: ((\forall (t: T).((ty3 g c0 
-u t) \to False)))).(\lambda (b: B).(\lambda (H4: (eq C (CHead c0 (Bind b) u) 
-(CHead c1 (Flat f) v))).(let H5 \def (eq_ind C (CHead c0 (Bind b) u) (\lambda 
-(ee: C).(match ee in C return (\lambda (_: C).Prop) with [(CSort _) 
-\Rightarrow False | (CHead _ k _) \Rightarrow (match k in K return (\lambda 
-(_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow 
-False])])) I (CHead c1 (Flat f) v) H4) in (False_ind (wf3 g c1 (CHead c2 
-(Bind Void) (TSort O))) H5)))))))))) (\lambda (c0: C).(\lambda (c2: 
-C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: (((eq C c0 (CHead c1 (Flat f) 
-v)) \to (wf3 g c1 c2)))).(\lambda (u: T).(\lambda (f0: F).(\lambda (H3: (eq C 
-(CHead c0 (Flat f0) u) (CHead c1 (Flat f) v))).(let H4 \def (f_equal C C 
-(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) 
-\Rightarrow c0 | (CHead c _ _) \Rightarrow c])) (CHead c0 (Flat f0) u) (CHead 
-c1 (Flat f) v) H3) in ((let H5 \def (f_equal C F (\lambda (e: C).(match e in 
-C return (\lambda (_: C).F) with [(CSort _) \Rightarrow f0 | (CHead _ k _) 
-\Rightarrow (match k in K return (\lambda (_: K).F) with [(Bind _) 
-\Rightarrow f0 | (Flat f1) \Rightarrow f1])])) (CHead c0 (Flat f0) u) (CHead 
-c1 (Flat f) v) H3) in ((let H6 \def (f_equal C T (\lambda (e: C).(match e in 
-C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) 
-\Rightarrow t])) (CHead c0 (Flat f0) u) (CHead c1 (Flat f) v) H3) in (\lambda 
-(_: (eq F f0 f)).(\lambda (H8: (eq C c0 c1)).(let H9 \def (eq_ind C c0 
-(\lambda (c: C).((eq C c (CHead c1 (Flat f) v)) \to (wf3 g c1 c2))) H2 c1 H8) 
-in (let H10 \def (eq_ind C c0 (\lambda (c: C).(wf3 g c c2)) H1 c1 H8) in 
-H10))))) H5)) H4))))))))) y x H0))) H)))))).
-(* COMMENTS
-Initial nodes: 737
-END *)
+F).(\lambda (H: (wf3 g (CHead c1 (Flat f) v) x)).(let TMP_1 \def (Flat f) in 
+(let TMP_2 \def (CHead c1 TMP_1 v) in (let TMP_3 \def (\lambda (c: C).(wf3 g 
+c x)) in (let TMP_4 \def (\lambda (_: C).(wf3 g c1 x)) in (let TMP_52 \def 
+(\lambda (y: C).(\lambda (H0: (wf3 g y x)).(let TMP_5 \def (\lambda (c: 
+C).(\lambda (c0: C).((eq C c (CHead c1 (Flat f) v)) \to (wf3 g c1 c0)))) in 
+(let TMP_12 \def (\lambda (m: nat).(\lambda (H1: (eq C (CSort m) (CHead c1 
+(Flat f) v))).(let TMP_6 \def (CSort m) in (let TMP_7 \def (\lambda (ee: 
+C).(match ee with [(CSort _) \Rightarrow True | (CHead _ _ _) \Rightarrow 
+False])) in (let TMP_8 \def (Flat f) in (let TMP_9 \def (CHead c1 TMP_8 v) in 
+(let H2 \def (eq_ind C TMP_6 TMP_7 I TMP_9 H1) in (let TMP_10 \def (CSort m) 
+in (let TMP_11 \def (wf3 g c1 TMP_10) in (False_ind TMP_11 H2)))))))))) in 
+(let TMP_21 \def (\lambda (c0: C).(\lambda (c2: C).(\lambda (_: (wf3 g c0 
+c2)).(\lambda (_: (((eq C c0 (CHead c1 (Flat f) v)) \to (wf3 g c1 
+c2)))).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 u t)).(\lambda 
+(b: B).(\lambda (H4: (eq C (CHead c0 (Bind b) u) (CHead c1 (Flat f) v))).(let 
+TMP_13 \def (Bind b) in (let TMP_14 \def (CHead c0 TMP_13 u) in (let TMP_15 
+\def (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ 
+k _) \Rightarrow (match k with [(Bind _) \Rightarrow True | (Flat _) 
+\Rightarrow False])])) in (let TMP_16 \def (Flat f) in (let TMP_17 \def 
+(CHead c1 TMP_16 v) in (let H5 \def (eq_ind C TMP_14 TMP_15 I TMP_17 H4) in 
+(let TMP_18 \def (Bind b) in (let TMP_19 \def (CHead c2 TMP_18 u) in (let 
+TMP_20 \def (wf3 g c1 TMP_19) in (False_ind TMP_20 H5))))))))))))))))))) in 
+(let TMP_31 \def (\lambda (c0: C).(\lambda (c2: C).(\lambda (_: (wf3 g c0 
+c2)).(\lambda (_: (((eq C c0 (CHead c1 (Flat f) v)) \to (wf3 g c1 
+c2)))).(\lambda (u: T).(\lambda (_: ((\forall (t: T).((ty3 g c0 u t) \to 
+False)))).(\lambda (b: B).(\lambda (H4: (eq C (CHead c0 (Bind b) u) (CHead c1 
+(Flat f) v))).(let TMP_22 \def (Bind b) in (let TMP_23 \def (CHead c0 TMP_22 
+u) in (let TMP_24 \def (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow 
+False | (CHead _ k _) \Rightarrow (match k with [(Bind _) \Rightarrow True | 
+(Flat _) \Rightarrow False])])) in (let TMP_25 \def (Flat f) in (let TMP_26 
+\def (CHead c1 TMP_25 v) in (let H5 \def (eq_ind C TMP_23 TMP_24 I TMP_26 H4) 
+in (let TMP_27 \def (Bind Void) in (let TMP_28 \def (TSort O) in (let TMP_29 
+\def (CHead c2 TMP_27 TMP_28) in (let TMP_30 \def (wf3 g c1 TMP_29) in 
+(False_ind TMP_30 H5))))))))))))))))))) in (let TMP_51 \def (\lambda (c0: 
+C).(\lambda (c2: C).(\lambda (H1: (wf3 g c0 c2)).(\lambda (H2: (((eq C c0 
+(CHead c1 (Flat f) v)) \to (wf3 g c1 c2)))).(\lambda (u: T).(\lambda (f0: 
+F).(\lambda (H3: (eq C (CHead c0 (Flat f0) u) (CHead c1 (Flat f) v))).(let 
+TMP_32 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow c0 | (CHead 
+c _ _) \Rightarrow c])) in (let TMP_33 \def (Flat f0) in (let TMP_34 \def 
+(CHead c0 TMP_33 u) in (let TMP_35 \def (Flat f) in (let TMP_36 \def (CHead 
+c1 TMP_35 v) in (let H4 \def (f_equal C C TMP_32 TMP_34 TMP_36 H3) in (let 
+TMP_37 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow f0 | (CHead 
+_ k _) \Rightarrow (match k with [(Bind _) \Rightarrow f0 | (Flat f1) 
+\Rightarrow f1])])) in (let TMP_38 \def (Flat f0) in (let TMP_39 \def (CHead 
+c0 TMP_38 u) in (let TMP_40 \def (Flat f) in (let TMP_41 \def (CHead c1 
+TMP_40 v) in (let H5 \def (f_equal C F TMP_37 TMP_39 TMP_41 H3) in (let 
+TMP_42 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow u | (CHead _ 
+_ t) \Rightarrow t])) in (let TMP_43 \def (Flat f0) in (let TMP_44 \def 
+(CHead c0 TMP_43 u) in (let TMP_45 \def (Flat f) in (let TMP_46 \def (CHead 
+c1 TMP_45 v) in (let H6 \def (f_equal C T TMP_42 TMP_44 TMP_46 H3) in (let 
+TMP_49 \def (\lambda (_: (eq F f0 f)).(\lambda (H8: (eq C c0 c1)).(let TMP_47 
+\def (\lambda (c: C).((eq C c (CHead c1 (Flat f) v)) \to (wf3 g c1 c2))) in 
+(let H9 \def (eq_ind C c0 TMP_47 H2 c1 H8) in (let TMP_48 \def (\lambda (c: 
+C).(wf3 g c c2)) in (let H10 \def (eq_ind C c0 TMP_48 H1 c1 H8) in H10)))))) 
+in (let TMP_50 \def (TMP_49 H5) in (TMP_50 H4)))))))))))))))))))))))))))) in 
+(wf3_ind g TMP_5 TMP_12 TMP_21 TMP_31 TMP_51 y x H0)))))))) in (insert_eq C 
+TMP_2 TMP_3 TMP_4 TMP_52 H))))))))))).
 
 theorem wf3_gen_head2:
  \forall (g: G).(\forall (x: C).(\forall (c: C).(\forall (v: T).(\forall (k: 
 K).((wf3 g x (CHead c k v)) \to (ex B (\lambda (b: B).(eq K k (Bind b)))))))))
 \def
  \lambda (g: G).(\lambda (x: C).(\lambda (c: C).(\lambda (v: T).(\lambda (k: 
-K).(\lambda (H: (wf3 g x (CHead c k v))).(insert_eq C (CHead c k v) (\lambda 
-(c0: C).(wf3 g x c0)) (\lambda (_: C).(ex B (\lambda (b: B).(eq K k (Bind 
-b))))) (\lambda (y: C).(\lambda (H0: (wf3 g x y)).(wf3_ind g (\lambda (_: 
-C).(\lambda (c1: C).((eq C c1 (CHead c k v)) \to (ex B (\lambda (b: B).(eq K 
-k (Bind b))))))) (\lambda (m: nat).(\lambda (H1: (eq C (CSort m) (CHead c k 
-v))).(let H2 \def (eq_ind C (CSort m) (\lambda (ee: C).(match ee in C return 
-(\lambda (_: C).Prop) with [(CSort _) \Rightarrow True | (CHead _ _ _) 
-\Rightarrow False])) I (CHead c k v) H1) in (False_ind (ex B (\lambda (b: 
-B).(eq K k (Bind b)))) H2)))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: 
-(wf3 g c1 c2)).(\lambda (H2: (((eq C c2 (CHead c k v)) \to (ex B (\lambda (b: 
-B).(eq K k (Bind b))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H3: (ty3 
-g c1 u t)).(\lambda (b: B).(\lambda (H4: (eq C (CHead c2 (Bind b) u) (CHead c 
-k v))).(let H5 \def (f_equal C C (\lambda (e: C).(match e in C return 
-(\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _ _) 
-\Rightarrow c0])) (CHead c2 (Bind b) u) (CHead c k v) H4) in ((let H6 \def 
-(f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: C).K) with 
-[(CSort _) \Rightarrow (Bind b) | (CHead _ k0 _) \Rightarrow k0])) (CHead c2 
-(Bind b) u) (CHead c k v) H4) in ((let H7 \def (f_equal C T (\lambda (e: 
-C).(match e in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow u | 
-(CHead _ _ t0) \Rightarrow t0])) (CHead c2 (Bind b) u) (CHead c k v) H4) in 
-(\lambda (H8: (eq K (Bind b) k)).(\lambda (H9: (eq C c2 c)).(let H10 \def 
-(eq_ind T u (\lambda (t0: T).(ty3 g c1 t0 t)) H3 v H7) in (let H11 \def 
-(eq_ind C c2 (\lambda (c0: C).((eq C c0 (CHead c k v)) \to (ex B (\lambda 
-(b0: B).(eq K k (Bind b0)))))) H2 c H9) in (let H12 \def (eq_ind C c2 
-(\lambda (c0: C).(wf3 g c1 c0)) H1 c H9) in (let H13 \def (eq_ind_r K k 
-(\lambda (k0: K).((eq C c (CHead c k0 v)) \to (ex B (\lambda (b0: B).(eq K k0 
-(Bind b0)))))) H11 (Bind b) H8) in (eq_ind K (Bind b) (\lambda (k0: K).(ex B 
-(\lambda (b0: B).(eq K k0 (Bind b0))))) (ex_intro B (\lambda (b0: B).(eq K 
-(Bind b) (Bind b0))) b (refl_equal K (Bind b))) k H8)))))))) H6)) 
-H5))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 
-c2)).(\lambda (H2: (((eq C c2 (CHead c k v)) \to (ex B (\lambda (b: B).(eq K 
-k (Bind b))))))).(\lambda (u: T).(\lambda (_: ((\forall (t: T).((ty3 g c1 u 
-t) \to False)))).(\lambda (_: B).(\lambda (H4: (eq C (CHead c2 (Bind Void) 
-(TSort O)) (CHead c k v))).(let H5 \def (f_equal C C (\lambda (e: C).(match e 
-in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow c2 | (CHead c0 _ 
-_) \Rightarrow c0])) (CHead c2 (Bind Void) (TSort O)) (CHead c k v) H4) in 
-((let H6 \def (f_equal C K (\lambda (e: C).(match e in C return (\lambda (_: 
-C).K) with [(CSort _) \Rightarrow (Bind Void) | (CHead _ k0 _) \Rightarrow 
-k0])) (CHead c2 (Bind Void) (TSort O)) (CHead c k v) H4) in ((let H7 \def 
-(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with 
-[(CSort _) \Rightarrow (TSort O) | (CHead _ _ t) \Rightarrow t])) (CHead c2 
-(Bind Void) (TSort O)) (CHead c k v) H4) in (\lambda (H8: (eq K (Bind Void) 
-k)).(\lambda (H9: (eq C c2 c)).(let H10 \def (eq_ind C c2 (\lambda (c0: 
-C).((eq C c0 (CHead c k v)) \to (ex B (\lambda (b0: B).(eq K k (Bind b0)))))) 
-H2 c H9) in (let H11 \def (eq_ind C c2 (\lambda (c0: C).(wf3 g c1 c0)) H1 c 
-H9) in (let H12 \def (eq_ind_r K k (\lambda (k0: K).((eq C c (CHead c k0 v)) 
-\to (ex B (\lambda (b0: B).(eq K k0 (Bind b0)))))) H10 (Bind Void) H8) in 
-(eq_ind K (Bind Void) (\lambda (k0: K).(ex B (\lambda (b0: B).(eq K k0 (Bind 
-b0))))) (let H13 \def (eq_ind_r T v (\lambda (t: T).((eq C c (CHead c (Bind 
-Void) t)) \to (ex B (\lambda (b0: B).(eq K (Bind Void) (Bind b0)))))) H12 
-(TSort O) H7) in (ex_intro B (\lambda (b0: B).(eq K (Bind Void) (Bind b0))) 
-Void (refl_equal K (Bind Void)))) k H8))))))) H6)) H5)))))))))) (\lambda (c1: 
+K).(\lambda (H: (wf3 g x (CHead c k v))).(let TMP_1 \def (CHead c k v) in 
+(let TMP_2 \def (\lambda (c0: C).(wf3 g x c0)) in (let TMP_5 \def (\lambda 
+(_: C).(let TMP_4 \def (\lambda (b: B).(let TMP_3 \def (Bind b) in (eq K k 
+TMP_3))) in (ex B TMP_4))) in (let TMP_102 \def (\lambda (y: C).(\lambda (H0: 
+(wf3 g x y)).(let TMP_8 \def (\lambda (_: C).(\lambda (c1: C).((eq C c1 
+(CHead c k v)) \to (let TMP_7 \def (\lambda (b: B).(let TMP_6 \def (Bind b) 
+in (eq K k TMP_6))) in (ex B TMP_7))))) in (let TMP_15 \def (\lambda (m: 
+nat).(\lambda (H1: (eq C (CSort m) (CHead c k v))).(let TMP_9 \def (CSort m) 
+in (let TMP_10 \def (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow 
+True | (CHead _ _ _) \Rightarrow False])) in (let TMP_11 \def (CHead c k v) 
+in (let H2 \def (eq_ind C TMP_9 TMP_10 I TMP_11 H1) in (let TMP_13 \def 
+(\lambda (b: B).(let TMP_12 \def (Bind b) in (eq K k TMP_12))) in (let TMP_14 
+\def (ex B TMP_13) in (False_ind TMP_14 H2))))))))) in (let TMP_49 \def 
+(\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: 
+(((eq C c2 (CHead c k v)) \to (ex B (\lambda (b: B).(eq K k (Bind 
+b))))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H3: (ty3 g c1 u 
+t)).(\lambda (b: B).(\lambda (H4: (eq C (CHead c2 (Bind b) u) (CHead c k 
+v))).(let TMP_16 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow c2 
+| (CHead c0 _ _) \Rightarrow c0])) in (let TMP_17 \def (Bind b) in (let 
+TMP_18 \def (CHead c2 TMP_17 u) in (let TMP_19 \def (CHead c k v) in (let H5 
+\def (f_equal C C TMP_16 TMP_18 TMP_19 H4) in (let TMP_20 \def (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow (Bind b) | (CHead _ k0 _) \Rightarrow 
+k0])) in (let TMP_21 \def (Bind b) in (let TMP_22 \def (CHead c2 TMP_21 u) in 
+(let TMP_23 \def (CHead c k v) in (let H6 \def (f_equal C K TMP_20 TMP_22 
+TMP_23 H4) in (let TMP_24 \def (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) in (let TMP_25 \def (Bind b) 
+in (let TMP_26 \def (CHead c2 TMP_25 u) in (let TMP_27 \def (CHead c k v) in 
+(let H7 \def (f_equal C T TMP_24 TMP_26 TMP_27 H4) in (let TMP_47 \def 
+(\lambda (H8: (eq K (Bind b) k)).(\lambda (H9: (eq C c2 c)).(let TMP_28 \def 
+(\lambda (t0: T).(ty3 g c1 t0 t)) in (let H10 \def (eq_ind T u TMP_28 H3 v 
+H7) in (let TMP_31 \def (\lambda (c0: C).((eq C c0 (CHead c k v)) \to (let 
+TMP_30 \def (\lambda (b0: B).(let TMP_29 \def (Bind b0) in (eq K k TMP_29))) 
+in (ex B TMP_30)))) in (let H11 \def (eq_ind C c2 TMP_31 H2 c H9) in (let 
+TMP_32 \def (\lambda (c0: C).(wf3 g c1 c0)) in (let H12 \def (eq_ind C c2 
+TMP_32 H1 c H9) in (let TMP_35 \def (\lambda (k0: K).((eq C c (CHead c k0 v)) 
+\to (let TMP_34 \def (\lambda (b0: B).(let TMP_33 \def (Bind b0) in (eq K k0 
+TMP_33))) in (ex B TMP_34)))) in (let TMP_36 \def (Bind b) in (let H13 \def 
+(eq_ind_r K k TMP_35 H11 TMP_36 H8) in (let TMP_37 \def (Bind b) in (let 
+TMP_40 \def (\lambda (k0: K).(let TMP_39 \def (\lambda (b0: B).(let TMP_38 
+\def (Bind b0) in (eq K k0 TMP_38))) in (ex B TMP_39))) in (let TMP_43 \def 
+(\lambda (b0: B).(let TMP_41 \def (Bind b) in (let TMP_42 \def (Bind b0) in 
+(eq K TMP_41 TMP_42)))) in (let TMP_44 \def (Bind b) in (let TMP_45 \def 
+(refl_equal K TMP_44) in (let TMP_46 \def (ex_intro B TMP_43 b TMP_45) in 
+(eq_ind K TMP_37 TMP_40 TMP_46 k H8)))))))))))))))))) in (let TMP_48 \def 
+(TMP_47 H6) in (TMP_48 H5))))))))))))))))))))))))))) in (let TMP_90 \def 
+(\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: 
+(((eq C c2 (CHead c k v)) \to (ex B (\lambda (b: B).(eq K k (Bind 
+b))))))).(\lambda (u: T).(\lambda (_: ((\forall (t: T).((ty3 g c1 u t) \to 
+False)))).(\lambda (_: B).(\lambda (H4: (eq C (CHead c2 (Bind Void) (TSort 
+O)) (CHead c k v))).(let TMP_50 \def (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0])) in (let TMP_51 \def (Bind 
+Void) in (let TMP_52 \def (TSort O) in (let TMP_53 \def (CHead c2 TMP_51 
+TMP_52) in (let TMP_54 \def (CHead c k v) in (let H5 \def (f_equal C C TMP_50 
+TMP_53 TMP_54 H4) in (let TMP_55 \def (\lambda (e: C).(match e with [(CSort 
+_) \Rightarrow (Bind Void) | (CHead _ k0 _) \Rightarrow k0])) in (let TMP_56 
+\def (Bind Void) in (let TMP_57 \def (TSort O) in (let TMP_58 \def (CHead c2 
+TMP_56 TMP_57) in (let TMP_59 \def (CHead c k v) in (let H6 \def (f_equal C K 
+TMP_55 TMP_58 TMP_59 H4) in (let TMP_60 \def (\lambda (e: C).(match e with 
+[(CSort _) \Rightarrow (TSort O) | (CHead _ _ t) \Rightarrow t])) in (let 
+TMP_61 \def (Bind Void) in (let TMP_62 \def (TSort O) in (let TMP_63 \def 
+(CHead c2 TMP_61 TMP_62) in (let TMP_64 \def (CHead c k v) in (let H7 \def 
+(f_equal C T TMP_60 TMP_63 TMP_64 H4) in (let TMP_88 \def (\lambda (H8: (eq K 
+(Bind Void) k)).(\lambda (H9: (eq C c2 c)).(let TMP_67 \def (\lambda (c0: 
+C).((eq C c0 (CHead c k v)) \to (let TMP_66 \def (\lambda (b0: B).(let TMP_65 
+\def (Bind b0) in (eq K k TMP_65))) in (ex B TMP_66)))) in (let H10 \def 
+(eq_ind C c2 TMP_67 H2 c H9) in (let TMP_68 \def (\lambda (c0: C).(wf3 g c1 
+c0)) in (let H11 \def (eq_ind C c2 TMP_68 H1 c H9) in (let TMP_71 \def 
+(\lambda (k0: K).((eq C c (CHead c k0 v)) \to (let TMP_70 \def (\lambda (b0: 
+B).(let TMP_69 \def (Bind b0) in (eq K k0 TMP_69))) in (ex B TMP_70)))) in 
+(let TMP_72 \def (Bind Void) in (let H12 \def (eq_ind_r K k TMP_71 H10 TMP_72 
+H8) in (let TMP_73 \def (Bind Void) in (let TMP_76 \def (\lambda (k0: K).(let 
+TMP_75 \def (\lambda (b0: B).(let TMP_74 \def (Bind b0) in (eq K k0 TMP_74))) 
+in (ex B TMP_75))) in (let TMP_80 \def (\lambda (t: T).((eq C c (CHead c 
+(Bind Void) t)) \to (let TMP_79 \def (\lambda (b0: B).(let TMP_77 \def (Bind 
+Void) in (let TMP_78 \def (Bind b0) in (eq K TMP_77 TMP_78)))) in (ex B 
+TMP_79)))) in (let TMP_81 \def (TSort O) in (let H13 \def (eq_ind_r T v 
+TMP_80 H12 TMP_81 H7) in (let TMP_84 \def (\lambda (b0: B).(let TMP_82 \def 
+(Bind Void) in (let TMP_83 \def (Bind b0) in (eq K TMP_82 TMP_83)))) in (let 
+TMP_85 \def (Bind Void) in (let TMP_86 \def (refl_equal K TMP_85) in (let 
+TMP_87 \def (ex_intro B TMP_84 Void TMP_86) in (eq_ind K TMP_73 TMP_76 TMP_87 
+k H8))))))))))))))))))) in (let TMP_89 \def (TMP_88 H6) in (TMP_89 
+H5))))))))))))))))))))))))))))) in (let TMP_101 \def (\lambda (c1: 
 C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: (((eq C c2 
 (CHead c k v)) \to (ex B (\lambda (b: B).(eq K k (Bind b))))))).(\lambda (_: 
-T).(\lambda (_: F).(\lambda (H3: (eq C c2 (CHead c k v))).(let H4 \def 
-(f_equal C C (\lambda (e: C).e) c2 (CHead c k v) H3) in (let H5 \def (eq_ind 
-C c2 (\lambda (c0: C).((eq C c0 (CHead c k v)) \to (ex B (\lambda (b: B).(eq 
-K k (Bind b)))))) H2 (CHead c k v) H4) in (let H6 \def (eq_ind C c2 (\lambda 
-(c0: C).(wf3 g c1 c0)) H1 (CHead c k v) H4) in (H5 (refl_equal C (CHead c k 
-v))))))))))))) x y H0))) H)))))).
-(* COMMENTS
-Initial nodes: 1225
-END *)
+T).(\lambda (_: F).(\lambda (H3: (eq C c2 (CHead c k v))).(let TMP_91 \def 
+(\lambda (e: C).e) in (let TMP_92 \def (CHead c k v) in (let H4 \def (f_equal 
+C C TMP_91 c2 TMP_92 H3) in (let TMP_95 \def (\lambda (c0: C).((eq C c0 
+(CHead c k v)) \to (let TMP_94 \def (\lambda (b: B).(let TMP_93 \def (Bind b) 
+in (eq K k TMP_93))) in (ex B TMP_94)))) in (let TMP_96 \def (CHead c k v) in 
+(let H5 \def (eq_ind C c2 TMP_95 H2 TMP_96 H4) in (let TMP_97 \def (\lambda 
+(c0: C).(wf3 g c1 c0)) in (let TMP_98 \def (CHead c k v) in (let H6 \def 
+(eq_ind C c2 TMP_97 H1 TMP_98 H4) in (let TMP_99 \def (CHead c k v) in (let 
+TMP_100 \def (refl_equal C TMP_99) in (H5 TMP_100))))))))))))))))))) in 
+(wf3_ind g TMP_8 TMP_15 TMP_49 TMP_90 TMP_101 x y H0)))))))) in (insert_eq C 
+TMP_1 TMP_2 TMP_5 TMP_102 H)))))))))).
+
+theorem wf3_mono:
+ \forall (g: G).(\forall (c: C).(\forall (c1: C).((wf3 g c c1) \to (\forall 
+(c2: C).((wf3 g c c2) \to (eq C c1 c2))))))
+\def
+ \lambda (g: G).(\lambda (c: C).(\lambda (c1: C).(\lambda (H: (wf3 g c 
+c1)).(let TMP_1 \def (\lambda (c0: C).(\lambda (c2: C).(\forall (c3: C).((wf3 
+g c0 c3) \to (eq C c2 c3))))) in (let TMP_7 \def (\lambda (m: nat).(\lambda 
+(c2: C).(\lambda (H0: (wf3 g (CSort m) c2)).(let H_y \def (wf3_gen_sort1 g c2 
+m H0) in (let TMP_2 \def (CSort m) in (let TMP_4 \def (\lambda (c0: C).(let 
+TMP_3 \def (CSort m) in (eq C TMP_3 c0))) in (let TMP_5 \def (CSort m) in 
+(let TMP_6 \def (refl_equal C TMP_5) in (eq_ind_r C TMP_2 TMP_4 TMP_6 c2 
+H_y))))))))) in (let TMP_70 \def (\lambda (c2: C).(\lambda (c3: C).(\lambda 
+(_: (wf3 g c2 c3)).(\lambda (H1: ((\forall (c4: C).((wf3 g c2 c4) \to (eq C 
+c3 c4))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H2: (ty3 g c2 u 
+t)).(\lambda (b: B).(\lambda (c0: C).(\lambda (H3: (wf3 g (CHead c2 (Bind b) 
+u) c0)).(let H_x \def (wf3_gen_bind1 g c2 c0 u b H3) in (let H4 \def H_x in 
+(let TMP_10 \def (\lambda (c4: C).(\lambda (_: T).(let TMP_8 \def (Bind b) in 
+(let TMP_9 \def (CHead c4 TMP_8 u) in (eq C c0 TMP_9))))) in (let TMP_11 \def 
+(\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) in (let TMP_12 \def (\lambda 
+(_: C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_13 \def (ex3_2 C T TMP_10 
+TMP_11 TMP_12) in (let TMP_17 \def (\lambda (c4: C).(let TMP_14 \def (Bind 
+Void) in (let TMP_15 \def (TSort O) in (let TMP_16 \def (CHead c4 TMP_14 
+TMP_15) in (eq C c0 TMP_16))))) in (let TMP_18 \def (\lambda (c4: C).(wf3 g 
+c2 c4)) in (let TMP_19 \def (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) 
+\to False))) in (let TMP_20 \def (ex3 C TMP_17 TMP_18 TMP_19) in (let TMP_21 
+\def (Bind b) in (let TMP_22 \def (CHead c3 TMP_21 u) in (let TMP_23 \def (eq 
+C TMP_22 c0) in (let TMP_45 \def (\lambda (H5: (ex3_2 C T (\lambda (c4: 
+C).(\lambda (_: T).(eq C c0 (CHead c4 (Bind b) u)))) (\lambda (c4: 
+C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_: C).(\lambda (w: T).(ty3 g c2 
+u w))))).(let TMP_26 \def (\lambda (c4: C).(\lambda (_: T).(let TMP_24 \def 
+(Bind b) in (let TMP_25 \def (CHead c4 TMP_24 u) in (eq C c0 TMP_25))))) in 
+(let TMP_27 \def (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) in (let 
+TMP_28 \def (\lambda (_: C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_29 
+\def (Bind b) in (let TMP_30 \def (CHead c3 TMP_29 u) in (let TMP_31 \def (eq 
+C TMP_30 c0) in (let TMP_44 \def (\lambda (x0: C).(\lambda (x1: T).(\lambda 
+(H6: (eq C c0 (CHead x0 (Bind b) u))).(\lambda (H7: (wf3 g c2 x0)).(\lambda 
+(_: (ty3 g c2 u x1)).(let TMP_32 \def (Bind b) in (let TMP_33 \def (CHead x0 
+TMP_32 u) in (let TMP_36 \def (\lambda (c4: C).(let TMP_34 \def (Bind b) in 
+(let TMP_35 \def (CHead c3 TMP_34 u) in (eq C TMP_35 c4)))) in (let TMP_37 
+\def (Bind b) in (let TMP_38 \def (Bind b) in (let TMP_39 \def (H1 x0 H7) in 
+(let TMP_40 \def (Bind b) in (let TMP_41 \def (refl_equal K TMP_40) in (let 
+TMP_42 \def (refl_equal T u) in (let TMP_43 \def (f_equal3 C K T C CHead c3 
+x0 TMP_37 TMP_38 u u TMP_39 TMP_41 TMP_42) in (eq_ind_r C TMP_33 TMP_36 
+TMP_43 c0 H6)))))))))))))))) in (ex3_2_ind C T TMP_26 TMP_27 TMP_28 TMP_31 
+TMP_44 H5))))))))) in (let TMP_69 \def (\lambda (H5: (ex3 C (\lambda (c4: 
+C).(eq C c0 (CHead c4 (Bind Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 
+c4)) (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) \to False))))).(let 
+TMP_49 \def (\lambda (c4: C).(let TMP_46 \def (Bind Void) in (let TMP_47 \def 
+(TSort O) in (let TMP_48 \def (CHead c4 TMP_46 TMP_47) in (eq C c0 
+TMP_48))))) in (let TMP_50 \def (\lambda (c4: C).(wf3 g c2 c4)) in (let 
+TMP_51 \def (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) \to False))) in 
+(let TMP_52 \def (Bind b) in (let TMP_53 \def (CHead c3 TMP_52 u) in (let 
+TMP_54 \def (eq C TMP_53 c0) in (let TMP_68 \def (\lambda (x0: C).(\lambda 
+(H6: (eq C c0 (CHead x0 (Bind Void) (TSort O)))).(\lambda (_: (wf3 g c2 
+x0)).(\lambda (H8: ((\forall (w: T).((ty3 g c2 u w) \to False)))).(let TMP_55 
+\def (Bind Void) in (let TMP_56 \def (TSort O) in (let TMP_57 \def (CHead x0 
+TMP_55 TMP_56) in (let TMP_60 \def (\lambda (c4: C).(let TMP_58 \def (Bind b) 
+in (let TMP_59 \def (CHead c3 TMP_58 u) in (eq C TMP_59 c4)))) in (let H_x0 
+\def (H8 t H2) in (let H9 \def H_x0 in (let TMP_61 \def (Bind b) in (let 
+TMP_62 \def (CHead c3 TMP_61 u) in (let TMP_63 \def (Bind Void) in (let 
+TMP_64 \def (TSort O) in (let TMP_65 \def (CHead x0 TMP_63 TMP_64) in (let 
+TMP_66 \def (eq C TMP_62 TMP_65) in (let TMP_67 \def (False_ind TMP_66 H9) in 
+(eq_ind_r C TMP_57 TMP_60 TMP_67 c0 H6)))))))))))))))))) in (ex3_ind C TMP_49 
+TMP_50 TMP_51 TMP_54 TMP_68 H5))))))))) in (or_ind TMP_13 TMP_20 TMP_23 
+TMP_45 TMP_69 H4)))))))))))))))))))))))))) in (let TMP_141 \def (\lambda (c2: 
+C).(\lambda (c3: C).(\lambda (_: (wf3 g c2 c3)).(\lambda (H1: ((\forall (c4: 
+C).((wf3 g c2 c4) \to (eq C c3 c4))))).(\lambda (u: T).(\lambda (H2: 
+((\forall (t: T).((ty3 g c2 u t) \to False)))).(\lambda (b: B).(\lambda (c0: 
+C).(\lambda (H3: (wf3 g (CHead c2 (Bind b) u) c0)).(let H_x \def 
+(wf3_gen_bind1 g c2 c0 u b H3) in (let H4 \def H_x in (let TMP_73 \def 
+(\lambda (c4: C).(\lambda (_: T).(let TMP_71 \def (Bind b) in (let TMP_72 
+\def (CHead c4 TMP_71 u) in (eq C c0 TMP_72))))) in (let TMP_74 \def (\lambda 
+(c4: C).(\lambda (_: T).(wf3 g c2 c4))) in (let TMP_75 \def (\lambda (_: 
+C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_76 \def (ex3_2 C T TMP_73 
+TMP_74 TMP_75) in (let TMP_80 \def (\lambda (c4: C).(let TMP_77 \def (Bind 
+Void) in (let TMP_78 \def (TSort O) in (let TMP_79 \def (CHead c4 TMP_77 
+TMP_78) in (eq C c0 TMP_79))))) in (let TMP_81 \def (\lambda (c4: C).(wf3 g 
+c2 c4)) in (let TMP_82 \def (\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) 
+\to False))) in (let TMP_83 \def (ex3 C TMP_80 TMP_81 TMP_82) in (let TMP_84 
+\def (Bind Void) in (let TMP_85 \def (TSort O) in (let TMP_86 \def (CHead c3 
+TMP_84 TMP_85) in (let TMP_87 \def (eq C TMP_86 c0) in (let TMP_111 \def 
+(\lambda (H5: (ex3_2 C T (\lambda (c4: C).(\lambda (_: T).(eq C c0 (CHead c4 
+(Bind b) u)))) (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_: 
+C).(\lambda (w: T).(ty3 g c2 u w))))).(let TMP_90 \def (\lambda (c4: 
+C).(\lambda (_: T).(let TMP_88 \def (Bind b) in (let TMP_89 \def (CHead c4 
+TMP_88 u) in (eq C c0 TMP_89))))) in (let TMP_91 \def (\lambda (c4: 
+C).(\lambda (_: T).(wf3 g c2 c4))) in (let TMP_92 \def (\lambda (_: 
+C).(\lambda (w: T).(ty3 g c2 u w))) in (let TMP_93 \def (Bind Void) in (let 
+TMP_94 \def (TSort O) in (let TMP_95 \def (CHead c3 TMP_93 TMP_94) in (let 
+TMP_96 \def (eq C TMP_95 c0) in (let TMP_110 \def (\lambda (x0: C).(\lambda 
+(x1: T).(\lambda (H6: (eq C c0 (CHead x0 (Bind b) u))).(\lambda (_: (wf3 g c2 
+x0)).(\lambda (H8: (ty3 g c2 u x1)).(let TMP_97 \def (Bind b) in (let TMP_98 
+\def (CHead x0 TMP_97 u) in (let TMP_102 \def (\lambda (c4: C).(let TMP_99 
+\def (Bind Void) in (let TMP_100 \def (TSort O) in (let TMP_101 \def (CHead 
+c3 TMP_99 TMP_100) in (eq C TMP_101 c4))))) in (let H_x0 \def (H2 x1 H8) in 
+(let H9 \def H_x0 in (let TMP_103 \def (Bind Void) in (let TMP_104 \def 
+(TSort O) in (let TMP_105 \def (CHead c3 TMP_103 TMP_104) in (let TMP_106 
+\def (Bind b) in (let TMP_107 \def (CHead x0 TMP_106 u) in (let TMP_108 \def 
+(eq C TMP_105 TMP_107) in (let TMP_109 \def (False_ind TMP_108 H9) in 
+(eq_ind_r C TMP_98 TMP_102 TMP_109 c0 H6)))))))))))))))))) in (ex3_2_ind C T 
+TMP_90 TMP_91 TMP_92 TMP_96 TMP_110 H5)))))))))) in (let TMP_140 \def 
+(\lambda (H5: (ex3 C (\lambda (c4: C).(eq C c0 (CHead c4 (Bind Void) (TSort 
+O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda (_: C).(\forall (w: T).((ty3 g 
+c2 u w) \to False))))).(let TMP_115 \def (\lambda (c4: C).(let TMP_112 \def 
+(Bind Void) in (let TMP_113 \def (TSort O) in (let TMP_114 \def (CHead c4 
+TMP_112 TMP_113) in (eq C c0 TMP_114))))) in (let TMP_116 \def (\lambda (c4: 
+C).(wf3 g c2 c4)) in (let TMP_117 \def (\lambda (_: C).(\forall (w: T).((ty3 
+g c2 u w) \to False))) in (let TMP_118 \def (Bind Void) in (let TMP_119 \def 
+(TSort O) in (let TMP_120 \def (CHead c3 TMP_118 TMP_119) in (let TMP_121 
+\def (eq C TMP_120 c0) in (let TMP_139 \def (\lambda (x0: C).(\lambda (H6: 
+(eq C c0 (CHead x0 (Bind Void) (TSort O)))).(\lambda (H7: (wf3 g c2 
+x0)).(\lambda (_: ((\forall (w: T).((ty3 g c2 u w) \to False)))).(let TMP_122 
+\def (Bind Void) in (let TMP_123 \def (TSort O) in (let TMP_124 \def (CHead 
+x0 TMP_122 TMP_123) in (let TMP_128 \def (\lambda (c4: C).(let TMP_125 \def 
+(Bind Void) in (let TMP_126 \def (TSort O) in (let TMP_127 \def (CHead c3 
+TMP_125 TMP_126) in (eq C TMP_127 c4))))) in (let TMP_129 \def (Bind Void) in 
+(let TMP_130 \def (Bind Void) in (let TMP_131 \def (TSort O) in (let TMP_132 
+\def (TSort O) in (let TMP_133 \def (H1 x0 H7) in (let TMP_134 \def (Bind 
+Void) in (let TMP_135 \def (refl_equal K TMP_134) in (let TMP_136 \def (TSort 
+O) in (let TMP_137 \def (refl_equal T TMP_136) in (let TMP_138 \def (f_equal3 
+C K T C CHead c3 x0 TMP_129 TMP_130 TMP_131 TMP_132 TMP_133 TMP_135 TMP_137) 
+in (eq_ind_r C TMP_124 TMP_128 TMP_138 c0 H6))))))))))))))))))) in (ex3_ind C 
+TMP_115 TMP_116 TMP_117 TMP_121 TMP_139 H5)))))))))) in (or_ind TMP_76 TMP_83 
+TMP_87 TMP_111 TMP_140 H4)))))))))))))))))))))))))) in (let TMP_142 \def 
+(\lambda (c2: C).(\lambda (c3: C).(\lambda (_: (wf3 g c2 c3)).(\lambda (H1: 
+((\forall (c4: C).((wf3 g c2 c4) \to (eq C c3 c4))))).(\lambda (u: 
+T).(\lambda (f: F).(\lambda (c0: C).(\lambda (H2: (wf3 g (CHead c2 (Flat f) 
+u) c0)).(let H_y \def (wf3_gen_flat1 g c2 c0 u f H2) in (H1 c0 H_y)))))))))) 
+in (wf3_ind g TMP_1 TMP_7 TMP_70 TMP_141 TMP_142 c c1 H))))))))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma
index 8a8f13780c806ac02a1fdefd6ad45bfeb9c013cc..d73b1f2763ac46779de15f621a05718ffca6f04c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/getl.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/wf3/clear.ma".
+include "basic_1/wf3/clear.ma".
 
-include "Basic-1/ty3/dec.ma".
+include "basic_1/ty3/dec.ma".
 
 theorem wf3_getl_conf:
  \forall (b: B).(\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall 
@@ -25,181 +25,302 @@ C).((wf3 g c1 c2) \to (\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda
 (d2: C).(getl i c2 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 
 d2)))))))))))))
 \def
- \lambda (b: B).(\lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: 
-C).(\forall (d1: C).(\forall (v: T).((getl n c1 (CHead d1 (Bind b) v)) \to 
-(\forall (g: G).(\forall (c2: C).((wf3 g c1 c2) \to (\forall (w: T).((ty3 g 
-d1 v w) \to (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind b) v))) 
-(\lambda (d2: C).(wf3 g d1 d2))))))))))))) (\lambda (c1: C).(\lambda (d1: 
-C).(\lambda (v: T).(\lambda (H: (getl O c1 (CHead d1 (Bind b) v))).(\lambda 
-(g: G).(\lambda (c2: C).(\lambda (H0: (wf3 g c1 c2)).(\lambda (w: T).(\lambda 
-(H1: (ty3 g d1 v w)).(let H_y \def (wf3_clear_conf c1 (CHead d1 (Bind b) v) 
-(getl_gen_O c1 (CHead d1 (Bind b) v) H) g c2 H0) in (let H_x \def 
-(wf3_gen_bind1 g d1 c2 v b H_y) in (let H2 \def H_x in (or_ind (ex3_2 C T 
-(\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda 
-(c3: C).(\lambda (_: T).(wf3 g d1 c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 
-g d1 v w0)))) (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort 
-O)))) (\lambda (c3: C).(wf3 g d1 c3)) (\lambda (_: C).(\forall (w0: T).((ty3 
-g d1 v w0) \to False)))) (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind 
-b) v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (H3: (ex3_2 C T (\lambda 
-(c3: C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: 
-C).(\lambda (_: T).(wf3 g d1 c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g d1 
-v w0))))).(ex3_2_ind C T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 
-(Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g d1 c3))) (\lambda (_: 
-C).(\lambda (w0: T).(ty3 g d1 v w0))) (ex2 C (\lambda (d2: C).(getl O c2 
-(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (x0: 
+ \lambda (b: B).(\lambda (i: nat).(let TMP_5 \def (\lambda (n: nat).(\forall 
+(c1: C).(\forall (d1: C).(\forall (v: T).((getl n c1 (CHead d1 (Bind b) v)) 
+\to (\forall (g: G).(\forall (c2: C).((wf3 g c1 c2) \to (\forall (w: T).((ty3 
+g d1 v w) \to (let TMP_3 \def (\lambda (d2: C).(let TMP_1 \def (Bind b) in 
+(let TMP_2 \def (CHead d2 TMP_1 v) in (getl n c2 TMP_2)))) in (let TMP_4 \def 
+(\lambda (d2: C).(wf3 g d1 d2)) in (ex2 C TMP_3 TMP_4))))))))))))) in (let 
+TMP_86 \def (\lambda (c1: C).(\lambda (d1: C).(\lambda (v: T).(\lambda (H: 
+(getl O c1 (CHead d1 (Bind b) v))).(\lambda (g: G).(\lambda (c2: C).(\lambda 
+(H0: (wf3 g c1 c2)).(\lambda (w: T).(\lambda (H1: (ty3 g d1 v w)).(let TMP_6 
+\def (Bind b) in (let TMP_7 \def (CHead d1 TMP_6 v) in (let TMP_8 \def (Bind 
+b) in (let TMP_9 \def (CHead d1 TMP_8 v) in (let TMP_10 \def (getl_gen_O c1 
+TMP_9 H) in (let H_y \def (wf3_clear_conf c1 TMP_7 TMP_10 g c2 H0) in (let 
+H_x \def (wf3_gen_bind1 g d1 c2 v b H_y) in (let H2 \def H_x in (let TMP_13 
+\def (\lambda (c3: C).(\lambda (_: T).(let TMP_11 \def (Bind b) in (let 
+TMP_12 \def (CHead c3 TMP_11 v) in (eq C c2 TMP_12))))) in (let TMP_14 \def 
+(\lambda (c3: C).(\lambda (_: T).(wf3 g d1 c3))) in (let TMP_15 \def (\lambda 
+(_: C).(\lambda (w0: T).(ty3 g d1 v w0))) in (let TMP_16 \def (ex3_2 C T 
+TMP_13 TMP_14 TMP_15) in (let TMP_20 \def (\lambda (c3: C).(let TMP_17 \def 
+(Bind Void) in (let TMP_18 \def (TSort O) in (let TMP_19 \def (CHead c3 
+TMP_17 TMP_18) in (eq C c2 TMP_19))))) in (let TMP_21 \def (\lambda (c3: 
+C).(wf3 g d1 c3)) in (let TMP_22 \def (\lambda (_: C).(\forall (w0: T).((ty3 
+g d1 v w0) \to False))) in (let TMP_23 \def (ex3 C TMP_20 TMP_21 TMP_22) in 
+(let TMP_26 \def (\lambda (d2: C).(let TMP_24 \def (Bind b) in (let TMP_25 
+\def (CHead d2 TMP_24 v) in (getl O c2 TMP_25)))) in (let TMP_27 \def 
+(\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_28 \def (ex2 C TMP_26 TMP_27) in 
+(let TMP_55 \def (\lambda (H3: (ex3_2 C T (\lambda (c3: C).(\lambda (_: 
+T).(eq C c2 (CHead c3 (Bind b) v)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g 
+d1 c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g d1 v w0))))).(let TMP_31 
+\def (\lambda (c3: C).(\lambda (_: T).(let TMP_29 \def (Bind b) in (let 
+TMP_30 \def (CHead c3 TMP_29 v) in (eq C c2 TMP_30))))) in (let TMP_32 \def 
+(\lambda (c3: C).(\lambda (_: T).(wf3 g d1 c3))) in (let TMP_33 \def (\lambda 
+(_: C).(\lambda (w0: T).(ty3 g d1 v w0))) in (let TMP_36 \def (\lambda (d2: 
+C).(let TMP_34 \def (Bind b) in (let TMP_35 \def (CHead d2 TMP_34 v) in (getl 
+O c2 TMP_35)))) in (let TMP_37 \def (\lambda (d2: C).(wf3 g d1 d2)) in (let 
+TMP_38 \def (ex2 C TMP_36 TMP_37) in (let TMP_54 \def (\lambda (x0: 
 C).(\lambda (x1: T).(\lambda (H4: (eq C c2 (CHead x0 (Bind b) v))).(\lambda 
-(H5: (wf3 g d1 x0)).(\lambda (_: (ty3 g d1 v x1)).(eq_ind_r C (CHead x0 (Bind 
-b) v) (\lambda (c: C).(ex2 C (\lambda (d2: C).(getl O c (CHead d2 (Bind b) 
-v))) (\lambda (d2: C).(wf3 g d1 d2)))) (ex_intro2 C (\lambda (d2: C).(getl O 
-(CHead x0 (Bind b) v) (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)) 
-x0 (getl_refl b x0 v) H5) c2 H4)))))) H3)) (\lambda (H3: (ex3 C (\lambda (c3: 
-C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g d1 
-c3)) (\lambda (_: C).(\forall (w0: T).((ty3 g d1 v w0) \to 
-False))))).(ex3_ind C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort 
-O)))) (\lambda (c3: C).(wf3 g d1 c3)) (\lambda (_: C).(\forall (w0: T).((ty3 
-g d1 v w0) \to False))) (ex2 C (\lambda (d2: C).(getl O c2 (CHead d2 (Bind b) 
-v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (x0: C).(\lambda (H4: (eq C c2 
-(CHead x0 (Bind Void) (TSort O)))).(\lambda (_: (wf3 g d1 x0)).(\lambda (H6: 
-((\forall (w0: T).((ty3 g d1 v w0) \to False)))).(eq_ind_r C (CHead x0 (Bind 
-Void) (TSort O)) (\lambda (c: C).(ex2 C (\lambda (d2: C).(getl O c (CHead d2 
-(Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))) (let H_x0 \def (H6 w H1) in 
-(let H7 \def H_x0 in (False_ind (ex2 C (\lambda (d2: C).(getl O (CHead x0 
-(Bind Void) (TSort O)) (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 
-d2))) H7))) c2 H4))))) H3)) H2))))))))))))) (\lambda (n: nat).(\lambda (H: 
-((\forall (c1: C).(\forall (d1: C).(\forall (v: T).((getl n c1 (CHead d1 
-(Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c1 c2) \to (\forall 
-(w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind 
-b) v))) (\lambda (d2: C).(wf3 g d1 d2)))))))))))))).(\lambda (c1: C).(C_ind 
-(\lambda (c: C).(\forall (d1: C).(\forall (v: T).((getl (S n) c (CHead d1 
-(Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c c2) \to (\forall 
-(w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 
-(Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))))))))))) (\lambda (n0: 
-nat).(\lambda (d1: C).(\lambda (v: T).(\lambda (H0: (getl (S n) (CSort n0) 
-(CHead d1 (Bind b) v))).(\lambda (g: G).(\lambda (c2: C).(\lambda (_: (wf3 g 
-(CSort n0) c2)).(\lambda (w: T).(\lambda (_: (ty3 g d1 v w)).(getl_gen_sort 
-n0 (S n) (CHead d1 (Bind b) v) H0 (ex2 C (\lambda (d2: C).(getl (S n) c2 
-(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))))))))))))) (\lambda 
-(c: C).(\lambda (H0: ((\forall (d1: C).(\forall (v: T).((getl (S n) c (CHead 
-d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c c2) \to 
-(\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl (S n) c2 
-(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))))))))))))).(\lambda 
-(k: K).(\lambda (t: T).(\lambda (d1: C).(\lambda (v: T).(\lambda (H1: (getl 
-(S n) (CHead c k t) (CHead d1 (Bind b) v))).(\lambda (g: G).(\lambda (c2: 
-C).(\lambda (H2: (wf3 g (CHead c k t) c2)).(\lambda (w: T).(\lambda (H3: (ty3 
-g d1 v w)).(K_ind (\lambda (k0: K).((wf3 g (CHead c k0 t) c2) \to ((getl (r 
-k0 n) c (CHead d1 (Bind b) v)) \to (ex2 C (\lambda (d2: C).(getl (S n) c2 
-(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))))) (\lambda (b0: 
-B).(\lambda (H4: (wf3 g (CHead c (Bind b0) t) c2)).(\lambda (H5: (getl (r 
-(Bind b0) n) c (CHead d1 (Bind b) v))).(let H_x \def (wf3_gen_bind1 g c c2 t 
-b0 H4) in (let H6 \def H_x in (or_ind (ex3_2 C T (\lambda (c3: C).(\lambda 
-(_: T).(eq C c2 (CHead c3 (Bind b0) t)))) (\lambda (c3: C).(\lambda (_: 
-T).(wf3 g c c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g c t w0)))) (ex3 C 
-(\lambda (c3: C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: 
-C).(wf3 g c c3)) (\lambda (_: C).(\forall (w0: T).((ty3 g c t w0) \to 
-False)))) (ex2 C (\lambda (d2: C).(getl (S n) c2 (CHead d2 (Bind b) v))) 
-(\lambda (d2: C).(wf3 g d1 d2))) (\lambda (H7: (ex3_2 C T (\lambda (c3: 
-C).(\lambda (_: T).(eq C c2 (CHead c3 (Bind b0) t)))) (\lambda (c3: 
-C).(\lambda (_: T).(wf3 g c c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g c t 
-w0))))).(ex3_2_ind C T (\lambda (c3: C).(\lambda (_: T).(eq C c2 (CHead c3 
-(Bind b0) t)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g c c3))) (\lambda (_: 
-C).(\lambda (w0: T).(ty3 g c t w0))) (ex2 C (\lambda (d2: C).(getl (S n) c2 
-(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2))) (\lambda (x0: 
-C).(\lambda (x1: T).(\lambda (H8: (eq C c2 (CHead x0 (Bind b0) t))).(\lambda 
-(H9: (wf3 g c x0)).(\lambda (_: (ty3 g c t x1)).(eq_ind_r C (CHead x0 (Bind 
-b0) t) (\lambda (c0: C).(ex2 C (\lambda (d2: C).(getl (S n) c0 (CHead d2 
-(Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))) (let H_x0 \def (H c d1 v H5 g 
-x0 H9 w H3) in (let H11 \def H_x0 in (ex2_ind C (\lambda (d2: C).(getl n x0 
-(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)) (ex2 C (\lambda (d2: 
-C).(getl (S n) (CHead x0 (Bind b0) t) (CHead d2 (Bind b) v))) (\lambda (d2: 
-C).(wf3 g d1 d2))) (\lambda (x: C).(\lambda (H12: (getl n x0 (CHead x (Bind 
-b) v))).(\lambda (H13: (wf3 g d1 x)).(ex_intro2 C (\lambda (d2: C).(getl (S 
-n) (CHead x0 (Bind b0) t) (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 
-d2)) x (getl_head (Bind b0) n x0 (CHead x (Bind b) v) H12 t) H13)))) H11))) 
-c2 H8)))))) H7)) (\lambda (H7: (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 
-(Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c c3)) (\lambda (_: 
-C).(\forall (w0: T).((ty3 g c t w0) \to False))))).(ex3_ind C (\lambda (c3: 
-C).(eq C c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g c c3)) 
-(\lambda (_: C).(\forall (w0: T).((ty3 g c t w0) \to False))) (ex2 C (\lambda 
-(d2: C).(getl (S n) c2 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 
-d2))) (\lambda (x0: C).(\lambda (H8: (eq C c2 (CHead x0 (Bind Void) (TSort 
-O)))).(\lambda (H9: (wf3 g c x0)).(\lambda (_: ((\forall (w0: T).((ty3 g c t 
-w0) \to False)))).(eq_ind_r C (CHead x0 (Bind Void) (TSort O)) (\lambda (c0: 
-C).(ex2 C (\lambda (d2: C).(getl (S n) c0 (CHead d2 (Bind b) v))) (\lambda 
-(d2: C).(wf3 g d1 d2)))) (let H_x0 \def (H c d1 v H5 g x0 H9 w H3) in (let 
-H11 \def H_x0 in (ex2_ind C (\lambda (d2: C).(getl n x0 (CHead d2 (Bind b) 
-v))) (\lambda (d2: C).(wf3 g d1 d2)) (ex2 C (\lambda (d2: C).(getl (S n) 
-(CHead x0 (Bind Void) (TSort O)) (CHead d2 (Bind b) v))) (\lambda (d2: 
-C).(wf3 g d1 d2))) (\lambda (x: C).(\lambda (H12: (getl n x0 (CHead x (Bind 
-b) v))).(\lambda (H13: (wf3 g d1 x)).(ex_intro2 C (\lambda (d2: C).(getl (S 
-n) (CHead x0 (Bind Void) (TSort O)) (CHead d2 (Bind b) v))) (\lambda (d2: 
-C).(wf3 g d1 d2)) x (getl_head (Bind Void) n x0 (CHead x (Bind b) v) H12 
-(TSort O)) H13)))) H11))) c2 H8))))) H7)) H6)))))) (\lambda (f: F).(\lambda 
-(H4: (wf3 g (CHead c (Flat f) t) c2)).(\lambda (H5: (getl (r (Flat f) n) c 
-(CHead d1 (Bind b) v))).(let H_y \def (wf3_gen_flat1 g c c2 t f H4) in (H0 d1 
-v H5 g c2 H_y w H3))))) k H2 (getl_gen_S k c (CHead d1 (Bind b) v) t n 
-H1)))))))))))))) c1)))) i)).
-(* COMMENTS
-Initial nodes: 2531
-END *)
+(H5: (wf3 g d1 x0)).(\lambda (_: (ty3 g d1 v x1)).(let TMP_39 \def (Bind b) 
+in (let TMP_40 \def (CHead x0 TMP_39 v) in (let TMP_45 \def (\lambda (c: 
+C).(let TMP_43 \def (\lambda (d2: C).(let TMP_41 \def (Bind b) in (let TMP_42 
+\def (CHead d2 TMP_41 v) in (getl O c TMP_42)))) in (let TMP_44 \def (\lambda 
+(d2: C).(wf3 g d1 d2)) in (ex2 C TMP_43 TMP_44)))) in (let TMP_50 \def 
+(\lambda (d2: C).(let TMP_46 \def (Bind b) in (let TMP_47 \def (CHead x0 
+TMP_46 v) in (let TMP_48 \def (Bind b) in (let TMP_49 \def (CHead d2 TMP_48 
+v) in (getl O TMP_47 TMP_49)))))) in (let TMP_51 \def (\lambda (d2: C).(wf3 g 
+d1 d2)) in (let TMP_52 \def (getl_refl b x0 v) in (let TMP_53 \def (ex_intro2 
+C TMP_50 TMP_51 x0 TMP_52 H5) in (eq_ind_r C TMP_40 TMP_45 TMP_53 c2 
+H4))))))))))))) in (ex3_2_ind C T TMP_31 TMP_32 TMP_33 TMP_38 TMP_54 
+H3))))))))) in (let TMP_85 \def (\lambda (H3: (ex3 C (\lambda (c3: C).(eq C 
+c2 (CHead c3 (Bind Void) (TSort O)))) (\lambda (c3: C).(wf3 g d1 c3)) 
+(\lambda (_: C).(\forall (w0: T).((ty3 g d1 v w0) \to False))))).(let TMP_59 
+\def (\lambda (c3: C).(let TMP_56 \def (Bind Void) in (let TMP_57 \def (TSort 
+O) in (let TMP_58 \def (CHead c3 TMP_56 TMP_57) in (eq C c2 TMP_58))))) in 
+(let TMP_60 \def (\lambda (c3: C).(wf3 g d1 c3)) in (let TMP_61 \def (\lambda 
+(_: C).(\forall (w0: T).((ty3 g d1 v w0) \to False))) in (let TMP_64 \def 
+(\lambda (d2: C).(let TMP_62 \def (Bind b) in (let TMP_63 \def (CHead d2 
+TMP_62 v) in (getl O c2 TMP_63)))) in (let TMP_65 \def (\lambda (d2: C).(wf3 
+g d1 d2)) in (let TMP_66 \def (ex2 C TMP_64 TMP_65) in (let TMP_84 \def 
+(\lambda (x0: C).(\lambda (H4: (eq C c2 (CHead x0 (Bind Void) (TSort 
+O)))).(\lambda (_: (wf3 g d1 x0)).(\lambda (H6: ((\forall (w0: T).((ty3 g d1 
+v w0) \to False)))).(let TMP_67 \def (Bind Void) in (let TMP_68 \def (TSort 
+O) in (let TMP_69 \def (CHead x0 TMP_67 TMP_68) in (let TMP_74 \def (\lambda 
+(c: C).(let TMP_72 \def (\lambda (d2: C).(let TMP_70 \def (Bind b) in (let 
+TMP_71 \def (CHead d2 TMP_70 v) in (getl O c TMP_71)))) in (let TMP_73 \def 
+(\lambda (d2: C).(wf3 g d1 d2)) in (ex2 C TMP_72 TMP_73)))) in (let H_x0 \def 
+(H6 w H1) in (let H7 \def H_x0 in (let TMP_80 \def (\lambda (d2: C).(let 
+TMP_75 \def (Bind Void) in (let TMP_76 \def (TSort O) in (let TMP_77 \def 
+(CHead x0 TMP_75 TMP_76) in (let TMP_78 \def (Bind b) in (let TMP_79 \def 
+(CHead d2 TMP_78 v) in (getl O TMP_77 TMP_79))))))) in (let TMP_81 \def 
+(\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_82 \def (ex2 C TMP_80 TMP_81) in 
+(let TMP_83 \def (False_ind TMP_82 H7) in (eq_ind_r C TMP_69 TMP_74 TMP_83 c2 
+H4))))))))))))))) in (ex3_ind C TMP_59 TMP_60 TMP_61 TMP_66 TMP_84 
+H3))))))))) in (or_ind TMP_16 TMP_23 TMP_28 TMP_55 TMP_85 
+H2))))))))))))))))))))))))))))))) in (let TMP_231 \def (\lambda (n: 
+nat).(\lambda (H: ((\forall (c1: C).(\forall (d1: C).(\forall (v: T).((getl n 
+c1 (CHead d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c1 c2) 
+\to (\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl n c2 
+(CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 d2)))))))))))))).(\lambda 
+(c1: C).(let TMP_92 \def (\lambda (c: C).(\forall (d1: C).(\forall (v: 
+T).((getl (S n) c (CHead d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2: 
+C).((wf3 g c c2) \to (\forall (w: T).((ty3 g d1 v w) \to (let TMP_90 \def 
+(\lambda (d2: C).(let TMP_87 \def (S n) in (let TMP_88 \def (Bind b) in (let 
+TMP_89 \def (CHead d2 TMP_88 v) in (getl TMP_87 c2 TMP_89))))) in (let TMP_91 
+\def (\lambda (d2: C).(wf3 g d1 d2)) in (ex2 C TMP_90 TMP_91)))))))))))) in 
+(let TMP_102 \def (\lambda (n0: nat).(\lambda (d1: C).(\lambda (v: 
+T).(\lambda (H0: (getl (S n) (CSort n0) (CHead d1 (Bind b) v))).(\lambda (g: 
+G).(\lambda (c2: C).(\lambda (_: (wf3 g (CSort n0) c2)).(\lambda (w: 
+T).(\lambda (_: (ty3 g d1 v w)).(let TMP_93 \def (S n) in (let TMP_94 \def 
+(Bind b) in (let TMP_95 \def (CHead d1 TMP_94 v) in (let TMP_99 \def (\lambda 
+(d2: C).(let TMP_96 \def (S n) in (let TMP_97 \def (Bind b) in (let TMP_98 
+\def (CHead d2 TMP_97 v) in (getl TMP_96 c2 TMP_98))))) in (let TMP_100 \def 
+(\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_101 \def (ex2 C TMP_99 TMP_100) 
+in (getl_gen_sort n0 TMP_93 TMP_95 H0 TMP_101)))))))))))))))) in (let TMP_230 
+\def (\lambda (c: C).(\lambda (H0: ((\forall (d1: C).(\forall (v: T).((getl 
+(S n) c (CHead d1 (Bind b) v)) \to (\forall (g: G).(\forall (c2: C).((wf3 g c 
+c2) \to (\forall (w: T).((ty3 g d1 v w) \to (ex2 C (\lambda (d2: C).(getl (S 
+n) c2 (CHead d2 (Bind b) v))) (\lambda (d2: C).(wf3 g d1 
+d2))))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (d1: C).(\lambda (v: 
+T).(\lambda (H1: (getl (S n) (CHead c k t) (CHead d1 (Bind b) v))).(\lambda 
+(g: G).(\lambda (c2: C).(\lambda (H2: (wf3 g (CHead c k t) c2)).(\lambda (w: 
+T).(\lambda (H3: (ty3 g d1 v w)).(let TMP_108 \def (\lambda (k0: K).((wf3 g 
+(CHead c k0 t) c2) \to ((getl (r k0 n) c (CHead d1 (Bind b) v)) \to (let 
+TMP_106 \def (\lambda (d2: C).(let TMP_103 \def (S n) in (let TMP_104 \def 
+(Bind b) in (let TMP_105 \def (CHead d2 TMP_104 v) in (getl TMP_103 c2 
+TMP_105))))) in (let TMP_107 \def (\lambda (d2: C).(wf3 g d1 d2)) in (ex2 C 
+TMP_106 TMP_107)))))) in (let TMP_225 \def (\lambda (b0: B).(\lambda (H4: 
+(wf3 g (CHead c (Bind b0) t) c2)).(\lambda (H5: (getl (r (Bind b0) n) c 
+(CHead d1 (Bind b) v))).(let H_x \def (wf3_gen_bind1 g c c2 t b0 H4) in (let 
+H6 \def H_x in (let TMP_111 \def (\lambda (c3: C).(\lambda (_: T).(let 
+TMP_109 \def (Bind b0) in (let TMP_110 \def (CHead c3 TMP_109 t) in (eq C c2 
+TMP_110))))) in (let TMP_112 \def (\lambda (c3: C).(\lambda (_: T).(wf3 g c 
+c3))) in (let TMP_113 \def (\lambda (_: C).(\lambda (w0: T).(ty3 g c t w0))) 
+in (let TMP_114 \def (ex3_2 C T TMP_111 TMP_112 TMP_113) in (let TMP_118 \def 
+(\lambda (c3: C).(let TMP_115 \def (Bind Void) in (let TMP_116 \def (TSort O) 
+in (let TMP_117 \def (CHead c3 TMP_115 TMP_116) in (eq C c2 TMP_117))))) in 
+(let TMP_119 \def (\lambda (c3: C).(wf3 g c c3)) in (let TMP_120 \def 
+(\lambda (_: C).(\forall (w0: T).((ty3 g c t w0) \to False))) in (let TMP_121 
+\def (ex3 C TMP_118 TMP_119 TMP_120) in (let TMP_125 \def (\lambda (d2: 
+C).(let TMP_122 \def (S n) in (let TMP_123 \def (Bind b) in (let TMP_124 \def 
+(CHead d2 TMP_123 v) in (getl TMP_122 c2 TMP_124))))) in (let TMP_126 \def 
+(\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_127 \def (ex2 C TMP_125 TMP_126) 
+in (let TMP_173 \def (\lambda (H7: (ex3_2 C T (\lambda (c3: C).(\lambda (_: 
+T).(eq C c2 (CHead c3 (Bind b0) t)))) (\lambda (c3: C).(\lambda (_: T).(wf3 g 
+c c3))) (\lambda (_: C).(\lambda (w0: T).(ty3 g c t w0))))).(let TMP_130 \def 
+(\lambda (c3: C).(\lambda (_: T).(let TMP_128 \def (Bind b0) in (let TMP_129 
+\def (CHead c3 TMP_128 t) in (eq C c2 TMP_129))))) in (let TMP_131 \def 
+(\lambda (c3: C).(\lambda (_: T).(wf3 g c c3))) in (let TMP_132 \def (\lambda 
+(_: C).(\lambda (w0: T).(ty3 g c t w0))) in (let TMP_136 \def (\lambda (d2: 
+C).(let TMP_133 \def (S n) in (let TMP_134 \def (Bind b) in (let TMP_135 \def 
+(CHead d2 TMP_134 v) in (getl TMP_133 c2 TMP_135))))) in (let TMP_137 \def 
+(\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_138 \def (ex2 C TMP_136 TMP_137) 
+in (let TMP_172 \def (\lambda (x0: C).(\lambda (x1: T).(\lambda (H8: (eq C c2 
+(CHead x0 (Bind b0) t))).(\lambda (H9: (wf3 g c x0)).(\lambda (_: (ty3 g c t 
+x1)).(let TMP_139 \def (Bind b0) in (let TMP_140 \def (CHead x0 TMP_139 t) in 
+(let TMP_146 \def (\lambda (c0: C).(let TMP_144 \def (\lambda (d2: C).(let 
+TMP_141 \def (S n) in (let TMP_142 \def (Bind b) in (let TMP_143 \def (CHead 
+d2 TMP_142 v) in (getl TMP_141 c0 TMP_143))))) in (let TMP_145 \def (\lambda 
+(d2: C).(wf3 g d1 d2)) in (ex2 C TMP_144 TMP_145)))) in (let H_x0 \def (H c 
+d1 v H5 g x0 H9 w H3) in (let H11 \def H_x0 in (let TMP_149 \def (\lambda 
+(d2: C).(let TMP_147 \def (Bind b) in (let TMP_148 \def (CHead d2 TMP_147 v) 
+in (getl n x0 TMP_148)))) in (let TMP_150 \def (\lambda (d2: C).(wf3 g d1 
+d2)) in (let TMP_156 \def (\lambda (d2: C).(let TMP_151 \def (S n) in (let 
+TMP_152 \def (Bind b0) in (let TMP_153 \def (CHead x0 TMP_152 t) in (let 
+TMP_154 \def (Bind b) in (let TMP_155 \def (CHead d2 TMP_154 v) in (getl 
+TMP_151 TMP_153 TMP_155))))))) in (let TMP_157 \def (\lambda (d2: C).(wf3 g 
+d1 d2)) in (let TMP_158 \def (ex2 C TMP_156 TMP_157) in (let TMP_170 \def 
+(\lambda (x: C).(\lambda (H12: (getl n x0 (CHead x (Bind b) v))).(\lambda 
+(H13: (wf3 g d1 x)).(let TMP_164 \def (\lambda (d2: C).(let TMP_159 \def (S 
+n) in (let TMP_160 \def (Bind b0) in (let TMP_161 \def (CHead x0 TMP_160 t) 
+in (let TMP_162 \def (Bind b) in (let TMP_163 \def (CHead d2 TMP_162 v) in 
+(getl TMP_159 TMP_161 TMP_163))))))) in (let TMP_165 \def (\lambda (d2: 
+C).(wf3 g d1 d2)) in (let TMP_166 \def (Bind b0) in (let TMP_167 \def (Bind 
+b) in (let TMP_168 \def (CHead x TMP_167 v) in (let TMP_169 \def (getl_head 
+TMP_166 n x0 TMP_168 H12 t) in (ex_intro2 C TMP_164 TMP_165 x TMP_169 
+H13)))))))))) in (let TMP_171 \def (ex2_ind C TMP_149 TMP_150 TMP_158 TMP_170 
+H11) in (eq_ind_r C TMP_140 TMP_146 TMP_171 c2 H8)))))))))))))))))) in 
+(ex3_2_ind C T TMP_130 TMP_131 TMP_132 TMP_138 TMP_172 H7))))))))) in (let 
+TMP_224 \def (\lambda (H7: (ex3 C (\lambda (c3: C).(eq C c2 (CHead c3 (Bind 
+Void) (TSort O)))) (\lambda (c3: C).(wf3 g c c3)) (\lambda (_: C).(\forall 
+(w0: T).((ty3 g c t w0) \to False))))).(let TMP_177 \def (\lambda (c3: 
+C).(let TMP_174 \def (Bind Void) in (let TMP_175 \def (TSort O) in (let 
+TMP_176 \def (CHead c3 TMP_174 TMP_175) in (eq C c2 TMP_176))))) in (let 
+TMP_178 \def (\lambda (c3: C).(wf3 g c c3)) in (let TMP_179 \def (\lambda (_: 
+C).(\forall (w0: T).((ty3 g c t w0) \to False))) in (let TMP_183 \def 
+(\lambda (d2: C).(let TMP_180 \def (S n) in (let TMP_181 \def (Bind b) in 
+(let TMP_182 \def (CHead d2 TMP_181 v) in (getl TMP_180 c2 TMP_182))))) in 
+(let TMP_184 \def (\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_185 \def (ex2 C 
+TMP_183 TMP_184) in (let TMP_223 \def (\lambda (x0: C).(\lambda (H8: (eq C c2 
+(CHead x0 (Bind Void) (TSort O)))).(\lambda (H9: (wf3 g c x0)).(\lambda (_: 
+((\forall (w0: T).((ty3 g c t w0) \to False)))).(let TMP_186 \def (Bind Void) 
+in (let TMP_187 \def (TSort O) in (let TMP_188 \def (CHead x0 TMP_186 
+TMP_187) in (let TMP_194 \def (\lambda (c0: C).(let TMP_192 \def (\lambda 
+(d2: C).(let TMP_189 \def (S n) in (let TMP_190 \def (Bind b) in (let TMP_191 
+\def (CHead d2 TMP_190 v) in (getl TMP_189 c0 TMP_191))))) in (let TMP_193 
+\def (\lambda (d2: C).(wf3 g d1 d2)) in (ex2 C TMP_192 TMP_193)))) in (let 
+H_x0 \def (H c d1 v H5 g x0 H9 w H3) in (let H11 \def H_x0 in (let TMP_197 
+\def (\lambda (d2: C).(let TMP_195 \def (Bind b) in (let TMP_196 \def (CHead 
+d2 TMP_195 v) in (getl n x0 TMP_196)))) in (let TMP_198 \def (\lambda (d2: 
+C).(wf3 g d1 d2)) in (let TMP_205 \def (\lambda (d2: C).(let TMP_199 \def (S 
+n) in (let TMP_200 \def (Bind Void) in (let TMP_201 \def (TSort O) in (let 
+TMP_202 \def (CHead x0 TMP_200 TMP_201) in (let TMP_203 \def (Bind b) in (let 
+TMP_204 \def (CHead d2 TMP_203 v) in (getl TMP_199 TMP_202 TMP_204)))))))) in 
+(let TMP_206 \def (\lambda (d2: C).(wf3 g d1 d2)) in (let TMP_207 \def (ex2 C 
+TMP_205 TMP_206) in (let TMP_221 \def (\lambda (x: C).(\lambda (H12: (getl n 
+x0 (CHead x (Bind b) v))).(\lambda (H13: (wf3 g d1 x)).(let TMP_214 \def 
+(\lambda (d2: C).(let TMP_208 \def (S n) in (let TMP_209 \def (Bind Void) in 
+(let TMP_210 \def (TSort O) in (let TMP_211 \def (CHead x0 TMP_209 TMP_210) 
+in (let TMP_212 \def (Bind b) in (let TMP_213 \def (CHead d2 TMP_212 v) in 
+(getl TMP_208 TMP_211 TMP_213)))))))) in (let TMP_215 \def (\lambda (d2: 
+C).(wf3 g d1 d2)) in (let TMP_216 \def (Bind Void) in (let TMP_217 \def (Bind 
+b) in (let TMP_218 \def (CHead x TMP_217 v) in (let TMP_219 \def (TSort O) in 
+(let TMP_220 \def (getl_head TMP_216 n x0 TMP_218 H12 TMP_219) in (ex_intro2 
+C TMP_214 TMP_215 x TMP_220 H13))))))))))) in (let TMP_222 \def (ex2_ind C 
+TMP_197 TMP_198 TMP_207 TMP_221 H11) in (eq_ind_r C TMP_188 TMP_194 TMP_222 
+c2 H8)))))))))))))))))) in (ex3_ind C TMP_177 TMP_178 TMP_179 TMP_185 TMP_223 
+H7))))))))) in (or_ind TMP_114 TMP_121 TMP_127 TMP_173 TMP_224 
+H6))))))))))))))))))) in (let TMP_226 \def (\lambda (f: F).(\lambda (H4: (wf3 
+g (CHead c (Flat f) t) c2)).(\lambda (H5: (getl (r (Flat f) n) c (CHead d1 
+(Bind b) v))).(let H_y \def (wf3_gen_flat1 g c c2 t f H4) in (H0 d1 v H5 g c2 
+H_y w H3))))) in (let TMP_227 \def (Bind b) in (let TMP_228 \def (CHead d1 
+TMP_227 v) in (let TMP_229 \def (getl_gen_S k c TMP_228 t n H1) in (K_ind 
+TMP_108 TMP_225 TMP_226 k H2 TMP_229))))))))))))))))))) in (C_ind TMP_92 
+TMP_102 TMP_230 c1))))))) in (nat_ind TMP_5 TMP_86 TMP_231 i))))).
 
 theorem getl_wf3_trans:
  \forall (i: nat).(\forall (c1: C).(\forall (d1: C).((getl i c1 d1) \to 
 (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: 
 C).(wf3 g c1 c2)) (\lambda (c2: C).(getl i c2 d2)))))))))
 \def
- \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (c1: C).(\forall (d1: 
-C).((getl n c1 d1) \to (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to 
-(ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(getl n c2 
-d2)))))))))) (\lambda (c1: C).(\lambda (d1: C).(\lambda (H: (getl O c1 
-d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (H0: (wf3 g d1 d2)).(let H_x 
-\def (clear_wf3_trans c1 d1 (getl_gen_O c1 d1 H) g d2 H0) in (let H1 \def H_x 
-in (ex2_ind C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(clear c2 d2)) 
-(ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(getl O c2 d2))) 
-(\lambda (x: C).(\lambda (H2: (wf3 g c1 x)).(\lambda (H3: (clear x 
-d2)).(ex_intro2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(getl O c2 
-d2)) x H2 (getl_intro O x d2 x (drop_refl x) H3))))) H1))))))))) (\lambda (n: 
-nat).(\lambda (H: ((\forall (c1: C).(\forall (d1: C).((getl n c1 d1) \to 
+ \lambda (i: nat).(let TMP_3 \def (\lambda (n: nat).(\forall (c1: C).(\forall 
+(d1: C).((getl n c1 d1) \to (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) 
+\to (let TMP_1 \def (\lambda (c2: C).(wf3 g c1 c2)) in (let TMP_2 \def 
+(\lambda (c2: C).(getl n c2 d2)) in (ex2 C TMP_1 TMP_2)))))))))) in (let 
+TMP_15 \def (\lambda (c1: C).(\lambda (d1: C).(\lambda (H: (getl O c1 
+d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (H0: (wf3 g d1 d2)).(let TMP_4 
+\def (getl_gen_O c1 d1 H) in (let H_x \def (clear_wf3_trans c1 d1 TMP_4 g d2 
+H0) in (let H1 \def H_x in (let TMP_5 \def (\lambda (c2: C).(wf3 g c1 c2)) in 
+(let TMP_6 \def (\lambda (c2: C).(clear c2 d2)) in (let TMP_7 \def (\lambda 
+(c2: C).(wf3 g c1 c2)) in (let TMP_8 \def (\lambda (c2: C).(getl O c2 d2)) in 
+(let TMP_9 \def (ex2 C TMP_7 TMP_8) in (let TMP_14 \def (\lambda (x: 
+C).(\lambda (H2: (wf3 g c1 x)).(\lambda (H3: (clear x d2)).(let TMP_10 \def 
+(\lambda (c2: C).(wf3 g c1 c2)) in (let TMP_11 \def (\lambda (c2: C).(getl O 
+c2 d2)) in (let TMP_12 \def (drop_refl x) in (let TMP_13 \def (getl_intro O x 
+d2 x TMP_12 H3) in (ex_intro2 C TMP_10 TMP_11 x H2 TMP_13)))))))) in (ex2_ind 
+C TMP_5 TMP_6 TMP_9 TMP_14 H1)))))))))))))))) in (let TMP_102 \def (\lambda 
+(n: nat).(\lambda (H: ((\forall (c1: C).(\forall (d1: C).((getl n c1 d1) \to 
 (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: 
 C).(wf3 g c1 c2)) (\lambda (c2: C).(getl n c2 d2))))))))))).(\lambda (c1: 
-C).(C_ind (\lambda (c: C).(\forall (d1: C).((getl (S n) c d1) \to (\forall 
-(g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda (c2: C).(wf3 g c 
-c2)) (\lambda (c2: C).(getl (S n) c2 d2))))))))) (\lambda (n0: nat).(\lambda 
-(d1: C).(\lambda (H0: (getl (S n) (CSort n0) d1)).(\lambda (g: G).(\lambda 
-(d2: C).(\lambda (_: (wf3 g d1 d2)).(getl_gen_sort n0 (S n) d1 H0 (ex2 C 
-(\lambda (c2: C).(wf3 g (CSort n0) c2)) (\lambda (c2: C).(getl (S n) c2 
-d2)))))))))) (\lambda (c: C).(\lambda (H0: ((\forall (d1: C).((getl (S n) c 
+C).(let TMP_19 \def (\lambda (c: C).(\forall (d1: C).((getl (S n) c d1) \to 
+(\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (let TMP_16 \def (\lambda 
+(c2: C).(wf3 g c c2)) in (let TMP_18 \def (\lambda (c2: C).(let TMP_17 \def 
+(S n) in (getl TMP_17 c2 d2))) in (ex2 C TMP_16 TMP_18))))))))) in (let 
+TMP_26 \def (\lambda (n0: nat).(\lambda (d1: C).(\lambda (H0: (getl (S n) 
+(CSort n0) d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (_: (wf3 g d1 
+d2)).(let TMP_20 \def (S n) in (let TMP_22 \def (\lambda (c2: C).(let TMP_21 
+\def (CSort n0) in (wf3 g TMP_21 c2))) in (let TMP_24 \def (\lambda (c2: 
+C).(let TMP_23 \def (S n) in (getl TMP_23 c2 d2))) in (let TMP_25 \def (ex2 C 
+TMP_22 TMP_24) in (getl_gen_sort n0 TMP_20 d1 H0 TMP_25))))))))))) in (let 
+TMP_101 \def (\lambda (c: C).(\lambda (H0: ((\forall (d1: C).((getl (S n) c 
 d1) \to (\forall (g: G).(\forall (d2: C).((wf3 g d1 d2) \to (ex2 C (\lambda 
 (c2: C).(wf3 g c c2)) (\lambda (c2: C).(getl (S n) c2 d2)))))))))).(\lambda 
 (k: K).(\lambda (t: T).(\lambda (d1: C).(\lambda (H1: (getl (S n) (CHead c k 
-t) d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (H2: (wf3 g d1 d2)).(K_ind 
-(\lambda (k0: K).((getl (r k0 n) c d1) \to (ex2 C (\lambda (c2: C).(wf3 g 
-(CHead c k0 t) c2)) (\lambda (c2: C).(getl (S n) c2 d2))))) (\lambda (b: 
+t) d1)).(\lambda (g: G).(\lambda (d2: C).(\lambda (H2: (wf3 g d1 d2)).(let 
+TMP_31 \def (\lambda (k0: K).((getl (r k0 n) c d1) \to (let TMP_28 \def 
+(\lambda (c2: C).(let TMP_27 \def (CHead c k0 t) in (wf3 g TMP_27 c2))) in 
+(let TMP_30 \def (\lambda (c2: C).(let TMP_29 \def (S n) in (getl TMP_29 c2 
+d2))) in (ex2 C TMP_28 TMP_30))))) in (let TMP_82 \def (\lambda (b: 
 B).(\lambda (H3: (getl (r (Bind b) n) c d1)).(let H_x \def (H c d1 H3 g d2 
-H2) in (let H4 \def H_x in (ex2_ind C (\lambda (c2: C).(wf3 g c c2)) (\lambda 
-(c2: C).(getl n c2 d2)) (ex2 C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) 
-c2)) (\lambda (c2: C).(getl (S n) c2 d2))) (\lambda (x: C).(\lambda (H5: (wf3 
-g c x)).(\lambda (H6: (getl n x d2)).(let H_x0 \def (ty3_inference g c t) in 
-(let H7 \def H_x0 in (or_ind (ex T (\lambda (t2: T).(ty3 g c t t2))) (\forall 
-(t2: T).((ty3 g c t t2) \to False)) (ex2 C (\lambda (c2: C).(wf3 g (CHead c 
-(Bind b) t) c2)) (\lambda (c2: C).(getl (S n) c2 d2))) (\lambda (H8: (ex T 
-(\lambda (t2: T).(ty3 g c t t2)))).(ex_ind T (\lambda (t2: T).(ty3 g c t t2)) 
-(ex2 C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2)) (\lambda (c2: 
-C).(getl (S n) c2 d2))) (\lambda (x0: T).(\lambda (H9: (ty3 g c t 
-x0)).(ex_intro2 C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2)) (\lambda 
-(c2: C).(getl (S n) c2 d2)) (CHead x (Bind b) t) (wf3_bind g c x H5 t x0 H9 
-b) (getl_head (Bind b) n x d2 H6 t)))) H8)) (\lambda (H8: ((\forall (t2: 
-T).((ty3 g c t t2) \to False)))).(ex_intro2 C (\lambda (c2: C).(wf3 g (CHead 
-c (Bind b) t) c2)) (\lambda (c2: C).(getl (S n) c2 d2)) (CHead x (Bind Void) 
-(TSort O)) (wf3_void g c x H5 t H8 b) (getl_head (Bind Void) n x d2 H6 (TSort 
-O)))) H7)))))) H4))))) (\lambda (f: F).(\lambda (H3: (getl (r (Flat f) n) c 
-d1)).(let H_x \def (H0 d1 H3 g d2 H2) in (let H4 \def H_x in (ex2_ind C 
-(\lambda (c2: C).(wf3 g c c2)) (\lambda (c2: C).(getl (S n) c2 d2)) (ex2 C 
-(\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2)) (\lambda (c2: C).(getl (S 
-n) c2 d2))) (\lambda (x: C).(\lambda (H5: (wf3 g c x)).(\lambda (H6: (getl (S 
-n) x d2)).(ex_intro2 C (\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2)) 
-(\lambda (c2: C).(getl (S n) c2 d2)) x (wf3_flat g c x H5 t f) H6)))) H4))))) 
-k (getl_gen_S k c d1 t n H1))))))))))) c1)))) i).
-(* COMMENTS
-Initial nodes: 1139
-END *)
+H2) in (let H4 \def H_x in (let TMP_32 \def (\lambda (c2: C).(wf3 g c c2)) in 
+(let TMP_33 \def (\lambda (c2: C).(getl n c2 d2)) in (let TMP_36 \def 
+(\lambda (c2: C).(let TMP_34 \def (Bind b) in (let TMP_35 \def (CHead c 
+TMP_34 t) in (wf3 g TMP_35 c2)))) in (let TMP_38 \def (\lambda (c2: C).(let 
+TMP_37 \def (S n) in (getl TMP_37 c2 d2))) in (let TMP_39 \def (ex2 C TMP_36 
+TMP_38) in (let TMP_81 \def (\lambda (x: C).(\lambda (H5: (wf3 g c 
+x)).(\lambda (H6: (getl n x d2)).(let H_x0 \def (ty3_inference g c t) in (let 
+H7 \def H_x0 in (let TMP_40 \def (\lambda (t2: T).(ty3 g c t t2)) in (let 
+TMP_41 \def (ex T TMP_40) in (let TMP_42 \def (\forall (t2: T).((ty3 g c t 
+t2) \to False)) in (let TMP_45 \def (\lambda (c2: C).(let TMP_43 \def (Bind 
+b) in (let TMP_44 \def (CHead c TMP_43 t) in (wf3 g TMP_44 c2)))) in (let 
+TMP_47 \def (\lambda (c2: C).(let TMP_46 \def (S n) in (getl TMP_46 c2 d2))) 
+in (let TMP_48 \def (ex2 C TMP_45 TMP_47) in (let TMP_67 \def (\lambda (H8: 
+(ex T (\lambda (t2: T).(ty3 g c t t2)))).(let TMP_49 \def (\lambda (t2: 
+T).(ty3 g c t t2)) in (let TMP_52 \def (\lambda (c2: C).(let TMP_50 \def 
+(Bind b) in (let TMP_51 \def (CHead c TMP_50 t) in (wf3 g TMP_51 c2)))) in 
+(let TMP_54 \def (\lambda (c2: C).(let TMP_53 \def (S n) in (getl TMP_53 c2 
+d2))) in (let TMP_55 \def (ex2 C TMP_52 TMP_54) in (let TMP_66 \def (\lambda 
+(x0: T).(\lambda (H9: (ty3 g c t x0)).(let TMP_58 \def (\lambda (c2: C).(let 
+TMP_56 \def (Bind b) in (let TMP_57 \def (CHead c TMP_56 t) in (wf3 g TMP_57 
+c2)))) in (let TMP_60 \def (\lambda (c2: C).(let TMP_59 \def (S n) in (getl 
+TMP_59 c2 d2))) in (let TMP_61 \def (Bind b) in (let TMP_62 \def (CHead x 
+TMP_61 t) in (let TMP_63 \def (wf3_bind g c x H5 t x0 H9 b) in (let TMP_64 
+\def (Bind b) in (let TMP_65 \def (getl_head TMP_64 n x d2 H6 t) in 
+(ex_intro2 C TMP_58 TMP_60 TMP_62 TMP_63 TMP_65)))))))))) in (ex_ind T TMP_49 
+TMP_55 TMP_66 H8))))))) in (let TMP_80 \def (\lambda (H8: ((\forall (t2: 
+T).((ty3 g c t t2) \to False)))).(let TMP_70 \def (\lambda (c2: C).(let 
+TMP_68 \def (Bind b) in (let TMP_69 \def (CHead c TMP_68 t) in (wf3 g TMP_69 
+c2)))) in (let TMP_72 \def (\lambda (c2: C).(let TMP_71 \def (S n) in (getl 
+TMP_71 c2 d2))) in (let TMP_73 \def (Bind Void) in (let TMP_74 \def (TSort O) 
+in (let TMP_75 \def (CHead x TMP_73 TMP_74) in (let TMP_76 \def (wf3_void g c 
+x H5 t H8 b) in (let TMP_77 \def (Bind Void) in (let TMP_78 \def (TSort O) in 
+(let TMP_79 \def (getl_head TMP_77 n x d2 H6 TMP_78) in (ex_intro2 C TMP_70 
+TMP_72 TMP_75 TMP_76 TMP_79))))))))))) in (or_ind TMP_41 TMP_42 TMP_48 TMP_67 
+TMP_80 H7)))))))))))))) in (ex2_ind C TMP_32 TMP_33 TMP_39 TMP_81 
+H4))))))))))) in (let TMP_99 \def (\lambda (f: F).(\lambda (H3: (getl (r 
+(Flat f) n) c d1)).(let H_x \def (H0 d1 H3 g d2 H2) in (let H4 \def H_x in 
+(let TMP_83 \def (\lambda (c2: C).(wf3 g c c2)) in (let TMP_85 \def (\lambda 
+(c2: C).(let TMP_84 \def (S n) in (getl TMP_84 c2 d2))) in (let TMP_88 \def 
+(\lambda (c2: C).(let TMP_86 \def (Flat f) in (let TMP_87 \def (CHead c 
+TMP_86 t) in (wf3 g TMP_87 c2)))) in (let TMP_90 \def (\lambda (c2: C).(let 
+TMP_89 \def (S n) in (getl TMP_89 c2 d2))) in (let TMP_91 \def (ex2 C TMP_88 
+TMP_90) in (let TMP_98 \def (\lambda (x: C).(\lambda (H5: (wf3 g c 
+x)).(\lambda (H6: (getl (S n) x d2)).(let TMP_94 \def (\lambda (c2: C).(let 
+TMP_92 \def (Flat f) in (let TMP_93 \def (CHead c TMP_92 t) in (wf3 g TMP_93 
+c2)))) in (let TMP_96 \def (\lambda (c2: C).(let TMP_95 \def (S n) in (getl 
+TMP_95 c2 d2))) in (let TMP_97 \def (wf3_flat g c x H5 t f) in (ex_intro2 C 
+TMP_94 TMP_96 x TMP_97 H6))))))) in (ex2_ind C TMP_83 TMP_85 TMP_91 TMP_98 
+H4))))))))))) in (let TMP_100 \def (getl_gen_S k c d1 t n H1) in (K_ind 
+TMP_31 TMP_82 TMP_99 k TMP_100)))))))))))))) in (C_ind TMP_19 TMP_26 TMP_101 
+c1))))))) in (nat_ind TMP_3 TMP_15 TMP_102 i)))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/props.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/props.ma
index 98a05c6378bbd46baa2bc1906d30b1148886dd09..4aabeb81eb53face819fb837ec20af1ca5922ebd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/wf3/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/props.ma
@@ -14,222 +14,221 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/wf3/ty3.ma".
+include "basic_1/wf3/ty3.ma".
 
-include "Basic-1/app/defs.ma".
-
-theorem wf3_mono:
- \forall (g: G).(\forall (c: C).(\forall (c1: C).((wf3 g c c1) \to (\forall 
-(c2: C).((wf3 g c c2) \to (eq C c1 c2))))))
-\def
- \lambda (g: G).(\lambda (c: C).(\lambda (c1: C).(\lambda (H: (wf3 g c 
-c1)).(wf3_ind g (\lambda (c0: C).(\lambda (c2: C).(\forall (c3: C).((wf3 g c0 
-c3) \to (eq C c2 c3))))) (\lambda (m: nat).(\lambda (c2: C).(\lambda (H0: 
-(wf3 g (CSort m) c2)).(let H_y \def (wf3_gen_sort1 g c2 m H0) in (eq_ind_r C 
-(CSort m) (\lambda (c0: C).(eq C (CSort m) c0)) (refl_equal C (CSort m)) c2 
-H_y))))) (\lambda (c2: C).(\lambda (c3: C).(\lambda (_: (wf3 g c2 
-c3)).(\lambda (H1: ((\forall (c4: C).((wf3 g c2 c4) \to (eq C c3 
-c4))))).(\lambda (u: T).(\lambda (t: T).(\lambda (H2: (ty3 g c2 u 
-t)).(\lambda (b: B).(\lambda (c0: C).(\lambda (H3: (wf3 g (CHead c2 (Bind b) 
-u) c0)).(let H_x \def (wf3_gen_bind1 g c2 c0 u b H3) in (let H4 \def H_x in 
-(or_ind (ex3_2 C T (\lambda (c4: C).(\lambda (_: T).(eq C c0 (CHead c4 (Bind 
-b) u)))) (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_: 
-C).(\lambda (w: T).(ty3 g c2 u w)))) (ex3 C (\lambda (c4: C).(eq C c0 (CHead 
-c4 (Bind Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda (_: 
-C).(\forall (w: T).((ty3 g c2 u w) \to False)))) (eq C (CHead c3 (Bind b) u) 
-c0) (\lambda (H5: (ex3_2 C T (\lambda (c4: C).(\lambda (_: T).(eq C c0 (CHead 
-c4 (Bind b) u)))) (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda 
-(_: C).(\lambda (w: T).(ty3 g c2 u w))))).(ex3_2_ind C T (\lambda (c4: 
-C).(\lambda (_: T).(eq C c0 (CHead c4 (Bind b) u)))) (\lambda (c4: 
-C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_: C).(\lambda (w: T).(ty3 g c2 
-u w))) (eq C (CHead c3 (Bind b) u) c0) (\lambda (x0: C).(\lambda (x1: 
-T).(\lambda (H6: (eq C c0 (CHead x0 (Bind b) u))).(\lambda (H7: (wf3 g c2 
-x0)).(\lambda (_: (ty3 g c2 u x1)).(eq_ind_r C (CHead x0 (Bind b) u) (\lambda 
-(c4: C).(eq C (CHead c3 (Bind b) u) c4)) (f_equal3 C K T C CHead c3 x0 (Bind 
-b) (Bind b) u u (H1 x0 H7) (refl_equal K (Bind b)) (refl_equal T u)) c0 
-H6)))))) H5)) (\lambda (H5: (ex3 C (\lambda (c4: C).(eq C c0 (CHead c4 (Bind 
-Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda (_: C).(\forall 
-(w: T).((ty3 g c2 u w) \to False))))).(ex3_ind C (\lambda (c4: C).(eq C c0 
-(CHead c4 (Bind Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda 
-(_: C).(\forall (w: T).((ty3 g c2 u w) \to False))) (eq C (CHead c3 (Bind b) 
-u) c0) (\lambda (x0: C).(\lambda (H6: (eq C c0 (CHead x0 (Bind Void) (TSort 
-O)))).(\lambda (_: (wf3 g c2 x0)).(\lambda (H8: ((\forall (w: T).((ty3 g c2 u 
-w) \to False)))).(eq_ind_r C (CHead x0 (Bind Void) (TSort O)) (\lambda (c4: 
-C).(eq C (CHead c3 (Bind b) u) c4)) (let H_x0 \def (H8 t H2) in (let H9 \def 
-H_x0 in (False_ind (eq C (CHead c3 (Bind b) u) (CHead x0 (Bind Void) (TSort 
-O))) H9))) c0 H6))))) H5)) H4))))))))))))) (\lambda (c2: C).(\lambda (c3: 
-C).(\lambda (_: (wf3 g c2 c3)).(\lambda (H1: ((\forall (c4: C).((wf3 g c2 c4) 
-\to (eq C c3 c4))))).(\lambda (u: T).(\lambda (H2: ((\forall (t: T).((ty3 g 
-c2 u t) \to False)))).(\lambda (b: B).(\lambda (c0: C).(\lambda (H3: (wf3 g 
-(CHead c2 (Bind b) u) c0)).(let H_x \def (wf3_gen_bind1 g c2 c0 u b H3) in 
-(let H4 \def H_x in (or_ind (ex3_2 C T (\lambda (c4: C).(\lambda (_: T).(eq C 
-c0 (CHead c4 (Bind b) u)))) (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) 
-(\lambda (_: C).(\lambda (w: T).(ty3 g c2 u w)))) (ex3 C (\lambda (c4: C).(eq 
-C c0 (CHead c4 (Bind Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) 
-(\lambda (_: C).(\forall (w: T).((ty3 g c2 u w) \to False)))) (eq C (CHead c3 
-(Bind Void) (TSort O)) c0) (\lambda (H5: (ex3_2 C T (\lambda (c4: C).(\lambda 
-(_: T).(eq C c0 (CHead c4 (Bind b) u)))) (\lambda (c4: C).(\lambda (_: 
-T).(wf3 g c2 c4))) (\lambda (_: C).(\lambda (w: T).(ty3 g c2 u 
-w))))).(ex3_2_ind C T (\lambda (c4: C).(\lambda (_: T).(eq C c0 (CHead c4 
-(Bind b) u)))) (\lambda (c4: C).(\lambda (_: T).(wf3 g c2 c4))) (\lambda (_: 
-C).(\lambda (w: T).(ty3 g c2 u w))) (eq C (CHead c3 (Bind Void) (TSort O)) 
-c0) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C c0 (CHead x0 (Bind 
-b) u))).(\lambda (_: (wf3 g c2 x0)).(\lambda (H8: (ty3 g c2 u x1)).(eq_ind_r 
-C (CHead x0 (Bind b) u) (\lambda (c4: C).(eq C (CHead c3 (Bind Void) (TSort 
-O)) c4)) (let H_x0 \def (H2 x1 H8) in (let H9 \def H_x0 in (False_ind (eq C 
-(CHead c3 (Bind Void) (TSort O)) (CHead x0 (Bind b) u)) H9))) c0 H6)))))) 
-H5)) (\lambda (H5: (ex3 C (\lambda (c4: C).(eq C c0 (CHead c4 (Bind Void) 
-(TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda (_: C).(\forall (w: 
-T).((ty3 g c2 u w) \to False))))).(ex3_ind C (\lambda (c4: C).(eq C c0 (CHead 
-c4 (Bind Void) (TSort O)))) (\lambda (c4: C).(wf3 g c2 c4)) (\lambda (_: 
-C).(\forall (w: T).((ty3 g c2 u w) \to False))) (eq C (CHead c3 (Bind Void) 
-(TSort O)) c0) (\lambda (x0: C).(\lambda (H6: (eq C c0 (CHead x0 (Bind Void) 
-(TSort O)))).(\lambda (H7: (wf3 g c2 x0)).(\lambda (_: ((\forall (w: T).((ty3 
-g c2 u w) \to False)))).(eq_ind_r C (CHead x0 (Bind Void) (TSort O)) (\lambda 
-(c4: C).(eq C (CHead c3 (Bind Void) (TSort O)) c4)) (f_equal3 C K T C CHead 
-c3 x0 (Bind Void) (Bind Void) (TSort O) (TSort O) (H1 x0 H7) (refl_equal K 
-(Bind Void)) (refl_equal T (TSort O))) c0 H6))))) H5)) H4)))))))))))) 
-(\lambda (c2: C).(\lambda (c3: C).(\lambda (_: (wf3 g c2 c3)).(\lambda (H1: 
-((\forall (c4: C).((wf3 g c2 c4) \to (eq C c3 c4))))).(\lambda (u: 
-T).(\lambda (f: F).(\lambda (c0: C).(\lambda (H2: (wf3 g (CHead c2 (Flat f) 
-u) c0)).(let H_y \def (wf3_gen_flat1 g c2 c0 u f H2) in (H1 c0 H_y)))))))))) 
-c c1 H)))).
-(* COMMENTS
-Initial nodes: 1555
-END *)
+include "basic_1/app/defs.ma".
 
 theorem wf3_total:
  \forall (g: G).(\forall (c1: C).(ex C (\lambda (c2: C).(wf3 g c1 c2))))
 \def
- \lambda (g: G).(\lambda (c1: C).(C_ind (\lambda (c: C).(ex C (\lambda (c2: 
-C).(wf3 g c c2)))) (\lambda (n: nat).(ex_intro C (\lambda (c2: C).(wf3 g 
-(CSort n) c2)) (CSort n) (wf3_sort g n))) (\lambda (c: C).(\lambda (H: (ex C 
-(\lambda (c2: C).(wf3 g c c2)))).(\lambda (k: K).(\lambda (t: T).(let H0 \def 
-H in (ex_ind C (\lambda (c2: C).(wf3 g c c2)) (ex C (\lambda (c2: C).(wf3 g 
-(CHead c k t) c2))) (\lambda (x: C).(\lambda (H1: (wf3 g c x)).(K_ind 
-(\lambda (k0: K).(ex C (\lambda (c2: C).(wf3 g (CHead c k0 t) c2)))) (\lambda 
-(b: B).(let H_x \def (ty3_inference g c t) in (let H2 \def H_x in (or_ind (ex 
-T (\lambda (t2: T).(ty3 g c t t2))) (\forall (t2: T).((ty3 g c t t2) \to 
-False)) (ex C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2))) (\lambda 
-(H3: (ex T (\lambda (t2: T).(ty3 g c t t2)))).(ex_ind T (\lambda (t2: T).(ty3 
-g c t t2)) (ex C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2))) (\lambda 
-(x0: T).(\lambda (H4: (ty3 g c t x0)).(ex_intro C (\lambda (c2: C).(wf3 g 
-(CHead c (Bind b) t) c2)) (CHead x (Bind b) t) (wf3_bind g c x H1 t x0 H4 
-b)))) H3)) (\lambda (H3: ((\forall (t2: T).((ty3 g c t t2) \to 
-False)))).(ex_intro C (\lambda (c2: C).(wf3 g (CHead c (Bind b) t) c2)) 
-(CHead x (Bind Void) (TSort O)) (wf3_void g c x H1 t H3 b))) H2)))) (\lambda 
-(f: F).(ex_intro C (\lambda (c2: C).(wf3 g (CHead c (Flat f) t) c2)) x 
-(wf3_flat g c x H1 t f))) k))) H0)))))) c1)).
-(* COMMENTS
-Initial nodes: 435
-END *)
+ \lambda (g: G).(\lambda (c1: C).(let TMP_2 \def (\lambda (c: C).(let TMP_1 
+\def (\lambda (c2: C).(wf3 g c c2)) in (ex C TMP_1))) in (let TMP_7 \def 
+(\lambda (n: nat).(let TMP_4 \def (\lambda (c2: C).(let TMP_3 \def (CSort n) 
+in (wf3 g TMP_3 c2))) in (let TMP_5 \def (CSort n) in (let TMP_6 \def 
+(wf3_sort g n) in (ex_intro C TMP_4 TMP_5 TMP_6))))) in (let TMP_50 \def 
+(\lambda (c: C).(\lambda (H: (ex C (\lambda (c2: C).(wf3 g c c2)))).(\lambda 
+(k: K).(\lambda (t: T).(let H0 \def H in (let TMP_8 \def (\lambda (c2: 
+C).(wf3 g c c2)) in (let TMP_10 \def (\lambda (c2: C).(let TMP_9 \def (CHead 
+c k t) in (wf3 g TMP_9 c2))) in (let TMP_11 \def (ex C TMP_10) in (let TMP_49 
+\def (\lambda (x: C).(\lambda (H1: (wf3 g c x)).(let TMP_14 \def (\lambda 
+(k0: K).(let TMP_13 \def (\lambda (c2: C).(let TMP_12 \def (CHead c k0 t) in 
+(wf3 g TMP_12 c2))) in (ex C TMP_13))) in (let TMP_43 \def (\lambda (b: 
+B).(let H_x \def (ty3_inference g c t) in (let H2 \def H_x in (let TMP_15 
+\def (\lambda (t2: T).(ty3 g c t t2)) in (let TMP_16 \def (ex T TMP_15) in 
+(let TMP_17 \def (\forall (t2: T).((ty3 g c t t2) \to False)) in (let TMP_20 
+\def (\lambda (c2: C).(let TMP_18 \def (Bind b) in (let TMP_19 \def (CHead c 
+TMP_18 t) in (wf3 g TMP_19 c2)))) in (let TMP_21 \def (ex C TMP_20) in (let 
+TMP_34 \def (\lambda (H3: (ex T (\lambda (t2: T).(ty3 g c t t2)))).(let 
+TMP_22 \def (\lambda (t2: T).(ty3 g c t t2)) in (let TMP_25 \def (\lambda 
+(c2: C).(let TMP_23 \def (Bind b) in (let TMP_24 \def (CHead c TMP_23 t) in 
+(wf3 g TMP_24 c2)))) in (let TMP_26 \def (ex C TMP_25) in (let TMP_33 \def 
+(\lambda (x0: T).(\lambda (H4: (ty3 g c t x0)).(let TMP_29 \def (\lambda (c2: 
+C).(let TMP_27 \def (Bind b) in (let TMP_28 \def (CHead c TMP_27 t) in (wf3 g 
+TMP_28 c2)))) in (let TMP_30 \def (Bind b) in (let TMP_31 \def (CHead x 
+TMP_30 t) in (let TMP_32 \def (wf3_bind g c x H1 t x0 H4 b) in (ex_intro C 
+TMP_29 TMP_31 TMP_32))))))) in (ex_ind T TMP_22 TMP_26 TMP_33 H3)))))) in 
+(let TMP_42 \def (\lambda (H3: ((\forall (t2: T).((ty3 g c t t2) \to 
+False)))).(let TMP_37 \def (\lambda (c2: C).(let TMP_35 \def (Bind b) in (let 
+TMP_36 \def (CHead c TMP_35 t) in (wf3 g TMP_36 c2)))) in (let TMP_38 \def 
+(Bind Void) in (let TMP_39 \def (TSort O) in (let TMP_40 \def (CHead x TMP_38 
+TMP_39) in (let TMP_41 \def (wf3_void g c x H1 t H3 b) in (ex_intro C TMP_37 
+TMP_40 TMP_41))))))) in (or_ind TMP_16 TMP_17 TMP_21 TMP_34 TMP_42 
+H2))))))))))) in (let TMP_48 \def (\lambda (f: F).(let TMP_46 \def (\lambda 
+(c2: C).(let TMP_44 \def (Flat f) in (let TMP_45 \def (CHead c TMP_44 t) in 
+(wf3 g TMP_45 c2)))) in (let TMP_47 \def (wf3_flat g c x H1 t f) in (ex_intro 
+C TMP_46 x TMP_47)))) in (K_ind TMP_14 TMP_43 TMP_48 k)))))) in (ex_ind C 
+TMP_8 TMP_11 TMP_49 H0)))))))))) in (C_ind TMP_2 TMP_7 TMP_50 c1))))).
 
 theorem ty3_shift1:
  \forall (g: G).(\forall (c: C).((wf3 g c c) \to (\forall (t1: T).(\forall 
 (t2: T).((ty3 g c t1 t2) \to (ty3 g (CSort (cbk c)) (app1 c t1) (app1 c 
 t2)))))))
 \def
- \lambda (g: G).(\lambda (c: C).(\lambda (H: (wf3 g c c)).(insert_eq C c 
-(\lambda (c0: C).(wf3 g c0 c)) (\lambda (c0: C).(\forall (t1: T).(\forall 
-(t2: T).((ty3 g c0 t1 t2) \to (ty3 g (CSort (cbk c0)) (app1 c0 t1) (app1 c0 
-t2)))))) (\lambda (y: C).(\lambda (H0: (wf3 g y c)).(wf3_ind g (\lambda (c0: 
+ \lambda (g: G).(\lambda (c: C).(\lambda (H: (wf3 g c c)).(let TMP_1 \def 
+(\lambda (c0: C).(wf3 g c0 c)) in (let TMP_6 \def (\lambda (c0: C).(\forall 
+(t1: T).(\forall (t2: T).((ty3 g c0 t1 t2) \to (let TMP_2 \def (cbk c0) in 
+(let TMP_3 \def (CSort TMP_2) in (let TMP_4 \def (app1 c0 t1) in (let TMP_5 
+\def (app1 c0 t2) in (ty3 g TMP_3 TMP_4 TMP_5))))))))) in (let TMP_180 \def 
+(\lambda (y: C).(\lambda (H0: (wf3 g y c)).(let TMP_11 \def (\lambda (c0: 
 C).(\lambda (c1: C).((eq C c0 c1) \to (\forall (t1: T).(\forall (t2: T).((ty3 
-g c0 t1 t2) \to (ty3 g (CSort (cbk c0)) (app1 c0 t1) (app1 c0 t2)))))))) 
-(\lambda (m: nat).(\lambda (_: (eq C (CSort m) (CSort m))).(\lambda (t1: 
-T).(\lambda (t2: T).(\lambda (H2: (ty3 g (CSort m) t1 t2)).H2))))) (\lambda 
-(c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: (((eq C 
-c1 c2) \to (\forall (t1: T).(\forall (t2: T).((ty3 g c1 t1 t2) \to (ty3 g 
-(CSort (cbk c1)) (app1 c1 t1) (app1 c1 t2)))))))).(\lambda (u: T).(\lambda 
-(t: T).(\lambda (H3: (ty3 g c1 u t)).(\lambda (b: B).(\lambda (H4: (eq C 
-(CHead c1 (Bind b) u) (CHead c2 (Bind b) u))).(\lambda (t1: T).(\lambda (t2: 
-T).(\lambda (H5: (ty3 g (CHead c1 (Bind b) u) t1 t2)).(let H6 \def (f_equal C 
-C (\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _) 
-\Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) (CHead c1 (Bind b) u) 
-(CHead c2 (Bind b) u) H4) in (let H7 \def (eq_ind_r C c2 (\lambda (c0: 
-C).((eq C c1 c0) \to (\forall (t3: T).(\forall (t4: T).((ty3 g c1 t3 t4) \to 
-(ty3 g (CSort (cbk c1)) (app1 c1 t3) (app1 c1 t4))))))) H2 c1 H6) in (let H8 
-\def (eq_ind_r C c2 (\lambda (c0: C).(wf3 g c1 c0)) H1 c1 H6) in (ex_ind T 
-(\lambda (t0: T).(ty3 g (CHead c1 (Bind b) u) t2 t0)) (ty3 g (CSort (cbk c1)) 
-(app1 c1 (THead (Bind b) u t1)) (app1 c1 (THead (Bind b) u t2))) (\lambda (x: 
-T).(\lambda (_: (ty3 g (CHead c1 (Bind b) u) t2 x)).(H7 (refl_equal C c1) 
-(THead (Bind b) u t1) (THead (Bind b) u t2) (ty3_bind g c1 u t H3 b t1 t2 
-H5)))) (ty3_correct g (CHead c1 (Bind b) u) t1 t2 H5))))))))))))))))) 
-(\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: 
-(((eq C c1 c2) \to (\forall (t1: T).(\forall (t2: T).((ty3 g c1 t1 t2) \to 
-(ty3 g (CSort (cbk c1)) (app1 c1 t1) (app1 c1 t2)))))))).(\lambda (u: 
-T).(\lambda (H3: ((\forall (t: T).((ty3 g c1 u t) \to False)))).(\lambda (b: 
-B).(\lambda (H4: (eq C (CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort 
-O)))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H5: (ty3 g (CHead c1 (Bind 
-b) u) t1 t2)).(let H6 \def (f_equal C C (\lambda (e: C).(match e in C return 
-(\lambda (_: C).C) with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) 
-\Rightarrow c0])) (CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O)) H4) 
-in ((let H7 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda 
-(_: C).B) with [(CSort _) \Rightarrow b | (CHead _ k _) \Rightarrow (match k 
-in K return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _) 
-\Rightarrow b])])) (CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O)) H4) 
-in ((let H8 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda 
-(_: C).T) with [(CSort _) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) 
-(CHead c1 (Bind b) u) (CHead c2 (Bind Void) (TSort O)) H4) in (\lambda (H9: 
-(eq B b Void)).(\lambda (H10: (eq C c1 c2)).(let H11 \def (eq_ind B b 
-(\lambda (b0: B).(ty3 g (CHead c1 (Bind b0) u) t1 t2)) H5 Void H9) in 
-(eq_ind_r B Void (\lambda (b0: B).(ty3 g (CSort (cbk (CHead c1 (Bind b0) u))) 
-(app1 (CHead c1 (Bind b0) u) t1) (app1 (CHead c1 (Bind b0) u) t2))) (let H12 
-\def (eq_ind T u (\lambda (t: T).(ty3 g (CHead c1 (Bind Void) t) t1 t2)) H11 
-(TSort O) H8) in (let H13 \def (eq_ind T u (\lambda (t: T).(\forall (t0: 
-T).((ty3 g c1 t t0) \to False))) H3 (TSort O) H8) in (eq_ind_r T (TSort O) 
-(\lambda (t: T).(ty3 g (CSort (cbk (CHead c1 (Bind Void) t))) (app1 (CHead c1 
-(Bind Void) t) t1) (app1 (CHead c1 (Bind Void) t) t2))) (let H14 \def 
-(eq_ind_r C c2 (\lambda (c0: C).((eq C c1 c0) \to (\forall (t3: T).(\forall 
-(t4: T).((ty3 g c1 t3 t4) \to (ty3 g (CSort (cbk c1)) (app1 c1 t3) (app1 c1 
-t4))))))) H2 c1 H10) in (let H15 \def (eq_ind_r C c2 (\lambda (c0: C).(wf3 g 
-c1 c0)) H1 c1 H10) in (ex_ind T (\lambda (t: T).(ty3 g (CHead c1 (Bind Void) 
-(TSort O)) t2 t)) (ty3 g (CSort (cbk c1)) (app1 c1 (THead (Bind Void) (TSort 
-O) t1)) (app1 c1 (THead (Bind Void) (TSort O) t2))) (\lambda (x: T).(\lambda 
-(_: (ty3 g (CHead c1 (Bind Void) (TSort O)) t2 x)).(H14 (refl_equal C c1) 
-(THead (Bind Void) (TSort O) t1) (THead (Bind Void) (TSort O) t2) (ty3_bind g 
-c1 (TSort O) (TSort (next g O)) (ty3_sort g c1 O) Void t1 t2 H12)))) 
-(ty3_correct g (CHead c1 (Bind Void) (TSort O)) t1 t2 H12)))) u H8))) b 
-H9))))) H7)) H6))))))))))))) (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: 
-(wf3 g c1 c2)).(\lambda (H2: (((eq C c1 c2) \to (\forall (t1: T).(\forall 
-(t2: T).((ty3 g c1 t1 t2) \to (ty3 g (CSort (cbk c1)) (app1 c1 t1) (app1 c1 
+g c0 t1 t2) \to (let TMP_7 \def (cbk c0) in (let TMP_8 \def (CSort TMP_7) in 
+(let TMP_9 \def (app1 c0 t1) in (let TMP_10 \def (app1 c0 t2) in (ty3 g TMP_8 
+TMP_9 TMP_10))))))))))) in (let TMP_12 \def (\lambda (m: nat).(\lambda (_: 
+(eq C (CSort m) (CSort m))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H2: 
+(ty3 g (CSort m) t1 t2)).H2))))) in (let TMP_46 \def (\lambda (c1: 
+C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 c2)).(\lambda (H2: (((eq C c1 c2) 
+\to (\forall (t1: T).(\forall (t2: T).((ty3 g c1 t1 t2) \to (ty3 g (CSort 
+(cbk c1)) (app1 c1 t1) (app1 c1 t2)))))))).(\lambda (u: T).(\lambda (t: 
+T).(\lambda (H3: (ty3 g c1 u t)).(\lambda (b: B).(\lambda (H4: (eq C (CHead 
+c1 (Bind b) u) (CHead c2 (Bind b) u))).(\lambda (t1: T).(\lambda (t2: 
+T).(\lambda (H5: (ty3 g (CHead c1 (Bind b) u) t1 t2)).(let TMP_13 \def 
+(\lambda (e: C).(match e with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) 
+\Rightarrow c0])) in (let TMP_14 \def (Bind b) in (let TMP_15 \def (CHead c1 
+TMP_14 u) in (let TMP_16 \def (Bind b) in (let TMP_17 \def (CHead c2 TMP_16 
+u) in (let H6 \def (f_equal C C TMP_13 TMP_15 TMP_17 H4) in (let TMP_22 \def 
+(\lambda (c0: C).((eq C c1 c0) \to (\forall (t3: T).(\forall (t4: T).((ty3 g 
+c1 t3 t4) \to (let TMP_18 \def (cbk c1) in (let TMP_19 \def (CSort TMP_18) in 
+(let TMP_20 \def (app1 c1 t3) in (let TMP_21 \def (app1 c1 t4) in (ty3 g 
+TMP_19 TMP_20 TMP_21)))))))))) in (let H7 \def (eq_ind_r C c2 TMP_22 H2 c1 
+H6) in (let TMP_23 \def (\lambda (c0: C).(wf3 g c1 c0)) in (let H8 \def 
+(eq_ind_r C c2 TMP_23 H1 c1 H6) in (let TMP_26 \def (\lambda (t0: T).(let 
+TMP_24 \def (Bind b) in (let TMP_25 \def (CHead c1 TMP_24 u) in (ty3 g TMP_25 
+t2 t0)))) in (let TMP_27 \def (cbk c1) in (let TMP_28 \def (CSort TMP_27) in 
+(let TMP_29 \def (Bind b) in (let TMP_30 \def (THead TMP_29 u t1) in (let 
+TMP_31 \def (app1 c1 TMP_30) in (let TMP_32 \def (Bind b) in (let TMP_33 \def 
+(THead TMP_32 u t2) in (let TMP_34 \def (app1 c1 TMP_33) in (let TMP_35 \def 
+(ty3 g TMP_28 TMP_31 TMP_34) in (let TMP_42 \def (\lambda (x: T).(\lambda (_: 
+(ty3 g (CHead c1 (Bind b) u) t2 x)).(let TMP_36 \def (refl_equal C c1) in 
+(let TMP_37 \def (Bind b) in (let TMP_38 \def (THead TMP_37 u t1) in (let 
+TMP_39 \def (Bind b) in (let TMP_40 \def (THead TMP_39 u t2) in (let TMP_41 
+\def (ty3_bind g c1 u t H3 b t1 t2 H5) in (H7 TMP_36 TMP_38 TMP_40 
+TMP_41))))))))) in (let TMP_43 \def (Bind b) in (let TMP_44 \def (CHead c1 
+TMP_43 u) in (let TMP_45 \def (ty3_correct g TMP_44 t1 t2 H5) in (ex_ind T 
+TMP_26 TMP_35 TMP_42 TMP_45))))))))))))))))))))))))))))))))))))) in (let 
+TMP_139 \def (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 
+c2)).(\lambda (H2: (((eq C c1 c2) \to (\forall (t1: T).(\forall (t2: T).((ty3 
+g c1 t1 t2) \to (ty3 g (CSort (cbk c1)) (app1 c1 t1) (app1 c1 
+t2)))))))).(\lambda (u: T).(\lambda (H3: ((\forall (t: T).((ty3 g c1 u t) \to 
+False)))).(\lambda (b: B).(\lambda (H4: (eq C (CHead c1 (Bind b) u) (CHead c2 
+(Bind Void) (TSort O)))).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H5: (ty3 
+g (CHead c1 (Bind b) u) t1 t2)).(let TMP_47 \def (\lambda (e: C).(match e 
+with [(CSort _) \Rightarrow c1 | (CHead c0 _ _) \Rightarrow c0])) in (let 
+TMP_48 \def (Bind b) in (let TMP_49 \def (CHead c1 TMP_48 u) in (let TMP_50 
+\def (Bind Void) in (let TMP_51 \def (TSort O) in (let TMP_52 \def (CHead c2 
+TMP_50 TMP_51) in (let H6 \def (f_equal C C TMP_47 TMP_49 TMP_52 H4) in (let 
+TMP_53 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow b | (CHead _ 
+k _) \Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _) 
+\Rightarrow b])])) in (let TMP_54 \def (Bind b) in (let TMP_55 \def (CHead c1 
+TMP_54 u) in (let TMP_56 \def (Bind Void) in (let TMP_57 \def (TSort O) in 
+(let TMP_58 \def (CHead c2 TMP_56 TMP_57) in (let H7 \def (f_equal C B TMP_53 
+TMP_55 TMP_58 H4) in (let TMP_59 \def (\lambda (e: C).(match e with [(CSort 
+_) \Rightarrow u | (CHead _ _ t) \Rightarrow t])) in (let TMP_60 \def (Bind 
+b) in (let TMP_61 \def (CHead c1 TMP_60 u) in (let TMP_62 \def (Bind Void) in 
+(let TMP_63 \def (TSort O) in (let TMP_64 \def (CHead c2 TMP_62 TMP_63) in 
+(let H8 \def (f_equal C T TMP_59 TMP_61 TMP_64 H4) in (let TMP_137 \def 
+(\lambda (H9: (eq B b Void)).(\lambda (H10: (eq C c1 c2)).(let TMP_67 \def 
+(\lambda (b0: B).(let TMP_65 \def (Bind b0) in (let TMP_66 \def (CHead c1 
+TMP_65 u) in (ty3 g TMP_66 t1 t2)))) in (let H11 \def (eq_ind B b TMP_67 H5 
+Void H9) in (let TMP_78 \def (\lambda (b0: B).(let TMP_68 \def (Bind b0) in 
+(let TMP_69 \def (CHead c1 TMP_68 u) in (let TMP_70 \def (cbk TMP_69) in (let 
+TMP_71 \def (CSort TMP_70) in (let TMP_72 \def (Bind b0) in (let TMP_73 \def 
+(CHead c1 TMP_72 u) in (let TMP_74 \def (app1 TMP_73 t1) in (let TMP_75 \def 
+(Bind b0) in (let TMP_76 \def (CHead c1 TMP_75 u) in (let TMP_77 \def (app1 
+TMP_76 t2) in (ty3 g TMP_71 TMP_74 TMP_77)))))))))))) in (let TMP_81 \def 
+(\lambda (t: T).(let TMP_79 \def (Bind Void) in (let TMP_80 \def (CHead c1 
+TMP_79 t) in (ty3 g TMP_80 t1 t2)))) in (let TMP_82 \def (TSort O) in (let 
+H12 \def (eq_ind T u TMP_81 H11 TMP_82 H8) in (let TMP_83 \def (\lambda (t: 
+T).(\forall (t0: T).((ty3 g c1 t t0) \to False))) in (let TMP_84 \def (TSort 
+O) in (let H13 \def (eq_ind T u TMP_83 H3 TMP_84 H8) in (let TMP_85 \def 
+(TSort O) in (let TMP_96 \def (\lambda (t: T).(let TMP_86 \def (Bind Void) in 
+(let TMP_87 \def (CHead c1 TMP_86 t) in (let TMP_88 \def (cbk TMP_87) in (let 
+TMP_89 \def (CSort TMP_88) in (let TMP_90 \def (Bind Void) in (let TMP_91 
+\def (CHead c1 TMP_90 t) in (let TMP_92 \def (app1 TMP_91 t1) in (let TMP_93 
+\def (Bind Void) in (let TMP_94 \def (CHead c1 TMP_93 t) in (let TMP_95 \def 
+(app1 TMP_94 t2) in (ty3 g TMP_89 TMP_92 TMP_95)))))))))))) in (let TMP_101 
+\def (\lambda (c0: C).((eq C c1 c0) \to (\forall (t3: T).(\forall (t4: 
+T).((ty3 g c1 t3 t4) \to (let TMP_97 \def (cbk c1) in (let TMP_98 \def (CSort 
+TMP_97) in (let TMP_99 \def (app1 c1 t3) in (let TMP_100 \def (app1 c1 t4) in 
+(ty3 g TMP_98 TMP_99 TMP_100)))))))))) in (let H14 \def (eq_ind_r C c2 
+TMP_101 H2 c1 H10) in (let TMP_102 \def (\lambda (c0: C).(wf3 g c1 c0)) in 
+(let H15 \def (eq_ind_r C c2 TMP_102 H1 c1 H10) in (let TMP_106 \def (\lambda 
+(t: T).(let TMP_103 \def (Bind Void) in (let TMP_104 \def (TSort O) in (let 
+TMP_105 \def (CHead c1 TMP_103 TMP_104) in (ty3 g TMP_105 t2 t))))) in (let 
+TMP_107 \def (cbk c1) in (let TMP_108 \def (CSort TMP_107) in (let TMP_109 
+\def (Bind Void) in (let TMP_110 \def (TSort O) in (let TMP_111 \def (THead 
+TMP_109 TMP_110 t1) in (let TMP_112 \def (app1 c1 TMP_111) in (let TMP_113 
+\def (Bind Void) in (let TMP_114 \def (TSort O) in (let TMP_115 \def (THead 
+TMP_113 TMP_114 t2) in (let TMP_116 \def (app1 c1 TMP_115) in (let TMP_117 
+\def (ty3 g TMP_108 TMP_112 TMP_116) in (let TMP_130 \def (\lambda (x: 
+T).(\lambda (_: (ty3 g (CHead c1 (Bind Void) (TSort O)) t2 x)).(let TMP_118 
+\def (refl_equal C c1) in (let TMP_119 \def (Bind Void) in (let TMP_120 \def 
+(TSort O) in (let TMP_121 \def (THead TMP_119 TMP_120 t1) in (let TMP_122 
+\def (Bind Void) in (let TMP_123 \def (TSort O) in (let TMP_124 \def (THead 
+TMP_122 TMP_123 t2) in (let TMP_125 \def (TSort O) in (let TMP_126 \def (next 
+g O) in (let TMP_127 \def (TSort TMP_126) in (let TMP_128 \def (ty3_sort g c1 
+O) in (let TMP_129 \def (ty3_bind g c1 TMP_125 TMP_127 TMP_128 Void t1 t2 
+H12) in (H14 TMP_118 TMP_121 TMP_124 TMP_129))))))))))))))) in (let TMP_131 
+\def (Bind Void) in (let TMP_132 \def (TSort O) in (let TMP_133 \def (CHead 
+c1 TMP_131 TMP_132) in (let TMP_134 \def (ty3_correct g TMP_133 t1 t2 H12) in 
+(let TMP_135 \def (ex_ind T TMP_106 TMP_117 TMP_130 TMP_134) in (let TMP_136 
+\def (eq_ind_r T TMP_85 TMP_96 TMP_135 u H8) in (eq_ind_r B Void TMP_78 
+TMP_136 b H9))))))))))))))))))))))))))))))))))))) in (let TMP_138 \def 
+(TMP_137 H7) in (TMP_138 H6))))))))))))))))))))))))))))))))))) in (let 
+TMP_179 \def (\lambda (c1: C).(\lambda (c2: C).(\lambda (H1: (wf3 g c1 
+c2)).(\lambda (H2: (((eq C c1 c2) \to (\forall (t1: T).(\forall (t2: T).((ty3 
+g c1 t1 t2) \to (ty3 g (CSort (cbk c1)) (app1 c1 t1) (app1 c1 
 t2)))))))).(\lambda (u: T).(\lambda (f: F).(\lambda (H3: (eq C (CHead c1 
 (Flat f) u) c2)).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g (CHead 
-c1 (Flat f) u) t1 t2)).(let H5 \def (f_equal C C (\lambda (e: C).e) (CHead c1 
-(Flat f) u) c2 H3) in (let H6 \def (eq_ind_r C c2 (\lambda (c0: C).((eq C c1 
-c0) \to (\forall (t3: T).(\forall (t4: T).((ty3 g c1 t3 t4) \to (ty3 g (CSort 
-(cbk c1)) (app1 c1 t3) (app1 c1 t4))))))) H2 (CHead c1 (Flat f) u) H5) in 
-(let H7 \def (eq_ind_r C c2 (\lambda (c0: C).(wf3 g c1 c0)) H1 (CHead c1 
-(Flat f) u) H5) in (let H_x \def (wf3_gen_head2 g c1 c1 u (Flat f) H7) in 
-(let H8 \def H_x in (ex_ind B (\lambda (b: B).(eq K (Flat f) (Bind b))) (ty3 
-g (CSort (cbk c1)) (app1 c1 (THead (Flat f) u t1)) (app1 c1 (THead (Flat f) u 
-t2))) (\lambda (x: B).(\lambda (H9: (eq K (Flat f) (Bind x))).(let H10 \def 
-(eq_ind K (Flat f) (\lambda (ee: K).(match ee in K return (\lambda (_: 
-K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])) I 
-(Bind x) H9) in (False_ind (ty3 g (CSort (cbk c1)) (app1 c1 (THead (Flat f) u 
-t1)) (app1 c1 (THead (Flat f) u t2))) H10)))) H8)))))))))))))))) y c H0))) 
-H))).
-(* COMMENTS
-Initial nodes: 1677
-END *)
+c1 (Flat f) u) t1 t2)).(let TMP_140 \def (\lambda (e: C).e) in (let TMP_141 
+\def (Flat f) in (let TMP_142 \def (CHead c1 TMP_141 u) in (let H5 \def 
+(f_equal C C TMP_140 TMP_142 c2 H3) in (let TMP_147 \def (\lambda (c0: 
+C).((eq C c1 c0) \to (\forall (t3: T).(\forall (t4: T).((ty3 g c1 t3 t4) \to 
+(let TMP_143 \def (cbk c1) in (let TMP_144 \def (CSort TMP_143) in (let 
+TMP_145 \def (app1 c1 t3) in (let TMP_146 \def (app1 c1 t4) in (ty3 g TMP_144 
+TMP_145 TMP_146)))))))))) in (let TMP_148 \def (Flat f) in (let TMP_149 \def 
+(CHead c1 TMP_148 u) in (let H6 \def (eq_ind_r C c2 TMP_147 H2 TMP_149 H5) in 
+(let TMP_150 \def (\lambda (c0: C).(wf3 g c1 c0)) in (let TMP_151 \def (Flat 
+f) in (let TMP_152 \def (CHead c1 TMP_151 u) in (let H7 \def (eq_ind_r C c2 
+TMP_150 H1 TMP_152 H5) in (let TMP_153 \def (Flat f) in (let H_x \def 
+(wf3_gen_head2 g c1 c1 u TMP_153 H7) in (let H8 \def H_x in (let TMP_156 \def 
+(\lambda (b: B).(let TMP_154 \def (Flat f) in (let TMP_155 \def (Bind b) in 
+(eq K TMP_154 TMP_155)))) in (let TMP_157 \def (cbk c1) in (let TMP_158 \def 
+(CSort TMP_157) in (let TMP_159 \def (Flat f) in (let TMP_160 \def (THead 
+TMP_159 u t1) in (let TMP_161 \def (app1 c1 TMP_160) in (let TMP_162 \def 
+(Flat f) in (let TMP_163 \def (THead TMP_162 u t2) in (let TMP_164 \def (app1 
+c1 TMP_163) in (let TMP_165 \def (ty3 g TMP_158 TMP_161 TMP_164) in (let 
+TMP_178 \def (\lambda (x: B).(\lambda (H9: (eq K (Flat f) (Bind x))).(let 
+TMP_166 \def (Flat f) in (let TMP_167 \def (\lambda (ee: K).(match ee with 
+[(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])) in (let TMP_168 
+\def (Bind x) in (let H10 \def (eq_ind K TMP_166 TMP_167 I TMP_168 H9) in 
+(let TMP_169 \def (cbk c1) in (let TMP_170 \def (CSort TMP_169) in (let 
+TMP_171 \def (Flat f) in (let TMP_172 \def (THead TMP_171 u t1) in (let 
+TMP_173 \def (app1 c1 TMP_172) in (let TMP_174 \def (Flat f) in (let TMP_175 
+\def (THead TMP_174 u t2) in (let TMP_176 \def (app1 c1 TMP_175) in (let 
+TMP_177 \def (ty3 g TMP_170 TMP_173 TMP_176) in (False_ind TMP_177 
+H10)))))))))))))))) in (ex_ind B TMP_156 TMP_165 TMP_178 
+H8))))))))))))))))))))))))))))))))))))) in (wf3_ind g TMP_11 TMP_12 TMP_46 
+TMP_139 TMP_179 y c H0)))))))) in (insert_eq C c TMP_1 TMP_6 TMP_180 H)))))).
 
 theorem wf3_idem:
  \forall (g: G).(\forall (c1: C).(\forall (c2: C).((wf3 g c1 c2) \to (wf3 g 
 c2 c2))))
 \def
  \lambda (g: G).(\lambda (c1: C).(\lambda (c2: C).(\lambda (H: (wf3 g c1 
-c2)).(wf3_ind g (\lambda (_: C).(\lambda (c0: C).(wf3 g c0 c0))) (\lambda (m: 
-nat).(wf3_sort g m)) (\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (wf3 g 
-c3 c4)).(\lambda (H1: (wf3 g c4 c4)).(\lambda (u: T).(\lambda (t: T).(\lambda 
-(H2: (ty3 g c3 u t)).(\lambda (b: B).(wf3_bind g c4 c4 H1 u t (wf3_ty3_conf g 
-c3 u t H2 c4 H0) b))))))))) (\lambda (c3: C).(\lambda (c4: C).(\lambda (_: 
-(wf3 g c3 c4)).(\lambda (H1: (wf3 g c4 c4)).(\lambda (u: T).(\lambda (_: 
-((\forall (t: T).((ty3 g c3 u t) \to False)))).(\lambda (_: B).(wf3_bind g c4 
-c4 H1 (TSort O) (TSort (next g O)) (ty3_sort g c4 O) Void)))))))) (\lambda 
-(c3: C).(\lambda (c4: C).(\lambda (_: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4 
-c4)).(\lambda (_: T).(\lambda (_: F).H1)))))) c1 c2 H)))).
-(* COMMENTS
-Initial nodes: 207
-END *)
+c2)).(let TMP_1 \def (\lambda (_: C).(\lambda (c0: C).(wf3 g c0 c0))) in (let 
+TMP_2 \def (\lambda (m: nat).(wf3_sort g m)) in (let TMP_4 \def (\lambda (c3: 
+C).(\lambda (c4: C).(\lambda (H0: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4 
+c4)).(\lambda (u: T).(\lambda (t: T).(\lambda (H2: (ty3 g c3 u t)).(\lambda 
+(b: B).(let TMP_3 \def (wf3_ty3_conf g c3 u t H2 c4 H0) in (wf3_bind g c4 c4 
+H1 u t TMP_3 b)))))))))) in (let TMP_9 \def (\lambda (c3: C).(\lambda (c4: 
+C).(\lambda (_: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4 c4)).(\lambda (u: 
+T).(\lambda (_: ((\forall (t: T).((ty3 g c3 u t) \to False)))).(\lambda (_: 
+B).(let TMP_5 \def (TSort O) in (let TMP_6 \def (next g O) in (let TMP_7 \def 
+(TSort TMP_6) in (let TMP_8 \def (ty3_sort g c4 O) in (wf3_bind g c4 c4 H1 
+TMP_5 TMP_7 TMP_8 Void)))))))))))) in (let TMP_10 \def (\lambda (c3: 
+C).(\lambda (c4: C).(\lambda (_: (wf3 g c3 c4)).(\lambda (H1: (wf3 g c4 
+c4)).(\lambda (_: T).(\lambda (_: F).H1)))))) in (wf3_ind g TMP_1 TMP_2 TMP_4 
+TMP_9 TMP_10 c1 c2 H))))))))).
 
 theorem wf3_ty3:
  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (u: T).((ty3 g c1 t 
@@ -237,12 +236,12 @@ u) \to (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(ty3 g c2 t
 u)))))))
 \def
  \lambda (g: G).(\lambda (c1: C).(\lambda (t: T).(\lambda (u: T).(\lambda (H: 
-(ty3 g c1 t u)).(let H_x \def (wf3_total g c1) in (let H0 \def H_x in (ex_ind 
-C (\lambda (c2: C).(wf3 g c1 c2)) (ex2 C (\lambda (c2: C).(wf3 g c1 c2)) 
-(\lambda (c2: C).(ty3 g c2 t u))) (\lambda (x: C).(\lambda (H1: (wf3 g c1 
-x)).(ex_intro2 C (\lambda (c2: C).(wf3 g c1 c2)) (\lambda (c2: C).(ty3 g c2 t 
-u)) x H1 (wf3_ty3_conf g c1 t u H x H1)))) H0))))))).
-(* COMMENTS
-Initial nodes: 123
-END *)
+(ty3 g c1 t u)).(let H_x \def (wf3_total g c1) in (let H0 \def H_x in (let 
+TMP_1 \def (\lambda (c2: C).(wf3 g c1 c2)) in (let TMP_2 \def (\lambda (c2: 
+C).(wf3 g c1 c2)) in (let TMP_3 \def (\lambda (c2: C).(ty3 g c2 t u)) in (let 
+TMP_4 \def (ex2 C TMP_2 TMP_3) in (let TMP_8 \def (\lambda (x: C).(\lambda 
+(H1: (wf3 g c1 x)).(let TMP_5 \def (\lambda (c2: C).(wf3 g c1 c2)) in (let 
+TMP_6 \def (\lambda (c2: C).(ty3 g c2 t u)) in (let TMP_7 \def (wf3_ty3_conf 
+g c1 t u H x H1) in (ex_intro2 C TMP_5 TMP_6 x H1 TMP_7)))))) in (ex_ind C 
+TMP_1 TMP_4 TMP_8 H0)))))))))))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma b/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma
index e47d4a2e0d1032ae1060f4939ae71eb30bf92efb..70dc78087d77cd9b17871f7102cc2c0688932d36 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/wf3/ty3.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/wf3/getl.ma".
+include "basic_1/wf3/getl.ma".
 
 theorem wf3_pr2_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr2 c1 
@@ -22,27 +22,28 @@ t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t1
 u) \to (pr2 c2 t1 t2)))))))))
 \def
  \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
-(H: (pr2 c1 t1 t2)).(pr2_ind (\lambda (c: C).(\lambda (t: T).(\lambda (t0: 
-T).(\forall (c2: C).((wf3 g c c2) \to (\forall (u: T).((ty3 g c t u) \to (pr2 
-c2 t t0)))))))) (\lambda (c: C).(\lambda (t3: T).(\lambda (t4: T).(\lambda 
-(H0: (pr0 t3 t4)).(\lambda (c2: C).(\lambda (_: (wf3 g c c2)).(\lambda (u: 
-T).(\lambda (_: (ty3 g c t3 u)).(pr2_free c2 t3 t4 H0))))))))) (\lambda (c: 
-C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c 
-(CHead d (Bind Abbr) u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: 
-(pr0 t3 t4)).(\lambda (t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (c2: 
-C).(\lambda (H3: (wf3 g c c2)).(\lambda (u0: T).(\lambda (H4: (ty3 g c t3 
-u0)).(let H_y \def (ty3_sred_pr0 t3 t4 H1 g c u0 H4) in (let H_x \def 
-(ty3_getl_subst0 g c t4 u0 H_y u t i H2 Abbr d u H0) in (let H5 \def H_x in 
-(ex_ind T (\lambda (w: T).(ty3 g d u w)) (pr2 c2 t3 t) (\lambda (x: 
-T).(\lambda (H6: (ty3 g d u x)).(let H_x0 \def (wf3_getl_conf Abbr i c d u H0 
-g c2 H3 x H6) in (let H7 \def H_x0 in (ex2_ind C (\lambda (d2: C).(getl i c2 
-(CHead d2 (Bind Abbr) u))) (\lambda (d2: C).(wf3 g d d2)) (pr2 c2 t3 t) 
-(\lambda (x0: C).(\lambda (H8: (getl i c2 (CHead x0 (Bind Abbr) u))).(\lambda 
-(_: (wf3 g d x0)).(pr2_delta c2 x0 u i H8 t3 t4 H1 t H2)))) H7))))) 
-H5)))))))))))))))))) c1 t1 t2 H))))).
-(* COMMENTS
-Initial nodes: 373
-END *)
+(H: (pr2 c1 t1 t2)).(let TMP_1 \def (\lambda (c: C).(\lambda (t: T).(\lambda 
+(t0: T).(\forall (c2: C).((wf3 g c c2) \to (\forall (u: T).((ty3 g c t u) \to 
+(pr2 c2 t t0)))))))) in (let TMP_2 \def (\lambda (c: C).(\lambda (t3: 
+T).(\lambda (t4: T).(\lambda (H0: (pr0 t3 t4)).(\lambda (c2: C).(\lambda (_: 
+(wf3 g c c2)).(\lambda (u: T).(\lambda (_: (ty3 g c t3 u)).(pr2_free c2 t3 t4 
+H0))))))))) in (let TMP_12 \def (\lambda (c: C).(\lambda (d: C).(\lambda (u: 
+T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abbr) 
+u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: (pr0 t3 t4)).(\lambda 
+(t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (c2: C).(\lambda (H3: (wf3 g 
+c c2)).(\lambda (u0: T).(\lambda (H4: (ty3 g c t3 u0)).(let H_y \def 
+(ty3_sred_pr0 t3 t4 H1 g c u0 H4) in (let H_x \def (ty3_getl_subst0 g c t4 u0 
+H_y u t i H2 Abbr d u H0) in (let H5 \def H_x in (let TMP_3 \def (\lambda (w: 
+T).(ty3 g d u w)) in (let TMP_4 \def (pr2 c2 t3 t) in (let TMP_11 \def 
+(\lambda (x: T).(\lambda (H6: (ty3 g d u x)).(let H_x0 \def (wf3_getl_conf 
+Abbr i c d u H0 g c2 H3 x H6) in (let H7 \def H_x0 in (let TMP_7 \def 
+(\lambda (d2: C).(let TMP_5 \def (Bind Abbr) in (let TMP_6 \def (CHead d2 
+TMP_5 u) in (getl i c2 TMP_6)))) in (let TMP_8 \def (\lambda (d2: C).(wf3 g d 
+d2)) in (let TMP_9 \def (pr2 c2 t3 t) in (let TMP_10 \def (\lambda (x0: 
+C).(\lambda (H8: (getl i c2 (CHead x0 (Bind Abbr) u))).(\lambda (_: (wf3 g d 
+x0)).(pr2_delta c2 x0 u i H8 t3 t4 H1 t H2)))) in (ex2_ind C TMP_7 TMP_8 
+TMP_9 TMP_10 H7))))))))) in (ex_ind T TMP_3 TMP_4 TMP_11 
+H5))))))))))))))))))))) in (pr2_ind TMP_1 TMP_2 TMP_12 c1 t1 t2 H)))))))).
 
 theorem wf3_pr3_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pr3 c1 
@@ -50,19 +51,18 @@ t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t1
 u) \to (pr3 c2 t1 t2)))))))))
 \def
  \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
-(H: (pr3 c1 t1 t2)).(pr3_ind c1 (\lambda (t: T).(\lambda (t0: T).(\forall 
+(H: (pr3 c1 t1 t2)).(let TMP_1 \def (\lambda (t: T).(\lambda (t0: T).(\forall 
 (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t u) \to (pr3 c2 t 
-t0))))))) (\lambda (t: T).(\lambda (c2: C).(\lambda (_: (wf3 g c1 
-c2)).(\lambda (u: T).(\lambda (_: (ty3 g c1 t u)).(pr3_refl c2 t)))))) 
-(\lambda (t3: T).(\lambda (t4: T).(\lambda (H0: (pr2 c1 t4 t3)).(\lambda (t5: 
-T).(\lambda (_: (pr3 c1 t3 t5)).(\lambda (H2: ((\forall (c2: C).((wf3 g c1 
-c2) \to (\forall (u: T).((ty3 g c1 t3 u) \to (pr3 c2 t3 t5))))))).(\lambda 
-(c2: C).(\lambda (H3: (wf3 g c1 c2)).(\lambda (u: T).(\lambda (H4: (ty3 g c1 
-t4 u)).(pr3_sing c2 t3 t4 (wf3_pr2_conf g c1 t4 t3 H0 c2 H3 u H4) t5 (H2 c2 
-H3 u (ty3_sred_pr2 c1 t4 t3 H0 g u H4))))))))))))) t1 t2 H))))).
-(* COMMENTS
-Initial nodes: 217
-END *)
+t0))))))) in (let TMP_2 \def (\lambda (t: T).(\lambda (c2: C).(\lambda (_: 
+(wf3 g c1 c2)).(\lambda (u: T).(\lambda (_: (ty3 g c1 t u)).(pr3_refl c2 
+t)))))) in (let TMP_6 \def (\lambda (t3: T).(\lambda (t4: T).(\lambda (H0: 
+(pr2 c1 t4 t3)).(\lambda (t5: T).(\lambda (_: (pr3 c1 t3 t5)).(\lambda (H2: 
+((\forall (c2: C).((wf3 g c1 c2) \to (\forall (u: T).((ty3 g c1 t3 u) \to 
+(pr3 c2 t3 t5))))))).(\lambda (c2: C).(\lambda (H3: (wf3 g c1 c2)).(\lambda 
+(u: T).(\lambda (H4: (ty3 g c1 t4 u)).(let TMP_3 \def (wf3_pr2_conf g c1 t4 
+t3 H0 c2 H3 u H4) in (let TMP_4 \def (ty3_sred_pr2 c1 t4 t3 H0 g u H4) in 
+(let TMP_5 \def (H2 c2 H3 u TMP_4) in (pr3_sing c2 t3 t4 TMP_3 t5 
+TMP_5)))))))))))))) in (pr3_ind c1 TMP_1 TMP_2 TMP_6 t1 t2 H)))))))).
 
 theorem wf3_pc3_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((pc3 c1 
@@ -72,67 +72,79 @@ u1) \to (\forall (u2: T).((ty3 g c1 t2 u2) \to (pc3 c2 t1 t2)))))))))))
  \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
 (H: (pc3 c1 t1 t2)).(\lambda (c2: C).(\lambda (H0: (wf3 g c1 c2)).(\lambda 
 (u1: T).(\lambda (H1: (ty3 g c1 t1 u1)).(\lambda (u2: T).(\lambda (H2: (ty3 g 
-c1 t2 u2)).(let H3 \def H in (ex2_ind T (\lambda (t: T).(pr3 c1 t1 t)) 
-(\lambda (t: T).(pr3 c1 t2 t)) (pc3 c2 t1 t2) (\lambda (x: T).(\lambda (H4: 
-(pr3 c1 t1 x)).(\lambda (H5: (pr3 c1 t2 x)).(pc3_pr3_t c2 t1 x (wf3_pr3_conf 
-g c1 t1 x H4 c2 H0 u1 H1) t2 (wf3_pr3_conf g c1 t2 x H5 c2 H0 u2 H2))))) 
-H3)))))))))))).
-(* COMMENTS
-Initial nodes: 153
-END *)
+c1 t2 u2)).(let H3 \def H in (let TMP_1 \def (\lambda (t: T).(pr3 c1 t1 t)) 
+in (let TMP_2 \def (\lambda (t: T).(pr3 c1 t2 t)) in (let TMP_3 \def (pc3 c2 
+t1 t2) in (let TMP_6 \def (\lambda (x: T).(\lambda (H4: (pr3 c1 t1 
+x)).(\lambda (H5: (pr3 c1 t2 x)).(let TMP_4 \def (wf3_pr3_conf g c1 t1 x H4 
+c2 H0 u1 H1) in (let TMP_5 \def (wf3_pr3_conf g c1 t2 x H5 c2 H0 u2 H2) in 
+(pc3_pr3_t c2 t1 x TMP_4 t2 TMP_5)))))) in (ex2_ind T TMP_1 TMP_2 TMP_3 TMP_6 
+H3)))))))))))))))).
 
 theorem wf3_ty3_conf:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1 
 t1 t2) \to (\forall (c2: C).((wf3 g c1 c2) \to (ty3 g c2 t1 t2)))))))
 \def
  \lambda (g: G).(\lambda (c1: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
-(H: (ty3 g c1 t1 t2)).(ty3_ind g (\lambda (c: C).(\lambda (t: T).(\lambda 
-(t0: T).(\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 t t0)))))) (\lambda (c: 
-C).(\lambda (t3: T).(\lambda (t: T).(\lambda (H0: (ty3 g c t3 t)).(\lambda 
-(H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 t3 t))))).(\lambda (u: 
-T).(\lambda (t4: T).(\lambda (H2: (ty3 g c u t4)).(\lambda (H3: ((\forall 
-(c2: C).((wf3 g c c2) \to (ty3 g c2 u t4))))).(\lambda (H4: (pc3 c t4 
-t3)).(\lambda (c2: C).(\lambda (H5: (wf3 g c c2)).(ex_ind T (\lambda (t0: 
-T).(ty3 g c t4 t0)) (ty3 g c2 u t3) (\lambda (x: T).(\lambda (H6: (ty3 g c t4 
-x)).(ty3_conv g c2 t3 t (H1 c2 H5) u t4 (H3 c2 H5) (wf3_pc3_conf g c t4 t3 H4 
-c2 H5 x H6 t H0)))) (ty3_correct g c u t4 H2)))))))))))))) (\lambda (c: 
-C).(\lambda (m: nat).(\lambda (c2: C).(\lambda (_: (wf3 g c c2)).(ty3_sort g 
-c2 m))))) (\lambda (n: nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: 
-T).(\lambda (H0: (getl n c (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda 
+(H: (ty3 g c1 t1 t2)).(let TMP_1 \def (\lambda (c: C).(\lambda (t: 
+T).(\lambda (t0: T).(\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 t t0)))))) 
+in (let TMP_9 \def (\lambda (c: C).(\lambda (t3: T).(\lambda (t: T).(\lambda 
+(H0: (ty3 g c t3 t)).(\lambda (H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g 
+c2 t3 t))))).(\lambda (u: T).(\lambda (t4: T).(\lambda (H2: (ty3 g c u 
+t4)).(\lambda (H3: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 u 
+t4))))).(\lambda (H4: (pc3 c t4 t3)).(\lambda (c2: C).(\lambda (H5: (wf3 g c 
+c2)).(let TMP_2 \def (\lambda (t0: T).(ty3 g c t4 t0)) in (let TMP_3 \def 
+(ty3 g c2 u t3) in (let TMP_7 \def (\lambda (x: T).(\lambda (H6: (ty3 g c t4 
+x)).(let TMP_4 \def (H1 c2 H5) in (let TMP_5 \def (H3 c2 H5) in (let TMP_6 
+\def (wf3_pc3_conf g c t4 t3 H4 c2 H5 x H6 t H0) in (ty3_conv g c2 t3 t TMP_4 
+u t4 TMP_5 TMP_6)))))) in (let TMP_8 \def (ty3_correct g c u t4 H2) in 
+(ex_ind T TMP_2 TMP_3 TMP_7 TMP_8))))))))))))))))) in (let TMP_10 \def 
+(\lambda (c: C).(\lambda (m: nat).(\lambda (c2: C).(\lambda (_: (wf3 g c 
+c2)).(ty3_sort g c2 m))))) in (let TMP_21 \def (\lambda (n: nat).(\lambda (c: 
+C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c (CHead d (Bind 
+Abbr) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: 
+((\forall (c2: C).((wf3 g d c2) \to (ty3 g c2 u t))))).(\lambda (c2: 
+C).(\lambda (H3: (wf3 g c c2)).(let H_x \def (wf3_getl_conf Abbr n c d u H0 g 
+c2 H3 t H1) in (let H4 \def H_x in (let TMP_13 \def (\lambda (d2: C).(let 
+TMP_11 \def (Bind Abbr) in (let TMP_12 \def (CHead d2 TMP_11 u) in (getl n c2 
+TMP_12)))) in (let TMP_14 \def (\lambda (d2: C).(wf3 g d d2)) in (let TMP_15 
+\def (TLRef n) in (let TMP_16 \def (S n) in (let TMP_17 \def (lift TMP_16 O 
+t) in (let TMP_18 \def (ty3 g c2 TMP_15 TMP_17) in (let TMP_20 \def (\lambda 
+(x: C).(\lambda (H5: (getl n c2 (CHead x (Bind Abbr) u))).(\lambda (H6: (wf3 
+g d x)).(let TMP_19 \def (H2 x H6) in (ty3_abbr g n c2 x u H5 t TMP_19))))) 
+in (ex2_ind C TMP_13 TMP_14 TMP_18 TMP_20 H4)))))))))))))))))))) in (let 
+TMP_32 \def (\lambda (n: nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: 
+T).(\lambda (H0: (getl n c (CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda 
 (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (c2: C).((wf3 g d c2) \to (ty3 g 
 c2 u t))))).(\lambda (c2: C).(\lambda (H3: (wf3 g c c2)).(let H_x \def 
-(wf3_getl_conf Abbr n c d u H0 g c2 H3 t H1) in (let H4 \def H_x in (ex2_ind 
-C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abbr) u))) (\lambda (d2: 
-C).(wf3 g d d2)) (ty3 g c2 (TLRef n) (lift (S n) O t)) (\lambda (x: 
-C).(\lambda (H5: (getl n c2 (CHead x (Bind Abbr) u))).(\lambda (H6: (wf3 g d 
-x)).(ty3_abbr g n c2 x u H5 t (H2 x H6))))) H4))))))))))))) (\lambda (n: 
-nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c 
-(CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u 
-t)).(\lambda (H2: ((\forall (c2: C).((wf3 g d c2) \to (ty3 g c2 u 
-t))))).(\lambda (c2: C).(\lambda (H3: (wf3 g c c2)).(let H_x \def 
-(wf3_getl_conf Abst n c d u H0 g c2 H3 t H1) in (let H4 \def H_x in (ex2_ind 
-C (\lambda (d2: C).(getl n c2 (CHead d2 (Bind Abst) u))) (\lambda (d2: 
-C).(wf3 g d d2)) (ty3 g c2 (TLRef n) (lift (S n) O u)) (\lambda (x: 
-C).(\lambda (H5: (getl n c2 (CHead x (Bind Abst) u))).(\lambda (H6: (wf3 g d 
-x)).(ty3_abst g n c2 x u H5 t (H2 x H6))))) H4))))))))))))) (\lambda (c: 
-C).(\lambda (u: T).(\lambda (t: T).(\lambda (H0: (ty3 g c u t)).(\lambda (H1: 
-((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 u t))))).(\lambda (b: 
-B).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (ty3 g (CHead c (Bind b) u) 
-t3 t4)).(\lambda (H3: ((\forall (c2: C).((wf3 g (CHead c (Bind b) u) c2) \to 
-(ty3 g c2 t3 t4))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c c2)).(ty3_bind g 
-c2 u t (H1 c2 H4) b t3 t4 (H3 (CHead c2 (Bind b) u) (wf3_bind g c c2 H4 u t 
-H0 b))))))))))))))) (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda 
-(_: (ty3 g c w u)).(\lambda (H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g 
-c2 w u))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead 
-(Bind Abst) u t))).(\lambda (H3: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g 
-c2 v (THead (Bind Abst) u t)))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c 
-c2)).(ty3_appl g c2 w u (H1 c2 H4) v t (H3 c2 H4))))))))))))) (\lambda (c: 
+(wf3_getl_conf Abst n c d u H0 g c2 H3 t H1) in (let H4 \def H_x in (let 
+TMP_24 \def (\lambda (d2: C).(let TMP_22 \def (Bind Abst) in (let TMP_23 \def 
+(CHead d2 TMP_22 u) in (getl n c2 TMP_23)))) in (let TMP_25 \def (\lambda 
+(d2: C).(wf3 g d d2)) in (let TMP_26 \def (TLRef n) in (let TMP_27 \def (S n) 
+in (let TMP_28 \def (lift TMP_27 O u) in (let TMP_29 \def (ty3 g c2 TMP_26 
+TMP_28) in (let TMP_31 \def (\lambda (x: C).(\lambda (H5: (getl n c2 (CHead x 
+(Bind Abst) u))).(\lambda (H6: (wf3 g d x)).(let TMP_30 \def (H2 x H6) in 
+(ty3_abst g n c2 x u H5 t TMP_30))))) in (ex2_ind C TMP_24 TMP_25 TMP_29 
+TMP_31 H4)))))))))))))))))))) in (let TMP_38 \def (\lambda (c: C).(\lambda 
+(u: T).(\lambda (t: T).(\lambda (H0: (ty3 g c u t)).(\lambda (H1: ((\forall 
+(c2: C).((wf3 g c c2) \to (ty3 g c2 u t))))).(\lambda (b: B).(\lambda (t3: 
+T).(\lambda (t4: T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t3 t4)).(\lambda 
+(H3: ((\forall (c2: C).((wf3 g (CHead c (Bind b) u) c2) \to (ty3 g c2 t3 
+t4))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c c2)).(let TMP_33 \def (H1 c2 
+H4) in (let TMP_34 \def (Bind b) in (let TMP_35 \def (CHead c2 TMP_34 u) in 
+(let TMP_36 \def (wf3_bind g c c2 H4 u t H0 b) in (let TMP_37 \def (H3 TMP_35 
+TMP_36) in (ty3_bind g c2 u t TMP_33 b t3 t4 TMP_37)))))))))))))))))) in (let 
+TMP_41 \def (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 
+g c w u)).(\lambda (H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 w 
+u))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead (Bind 
+Abst) u t))).(\lambda (H3: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 v 
+(THead (Bind Abst) u t)))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c 
+c2)).(let TMP_39 \def (H1 c2 H4) in (let TMP_40 \def (H3 c2 H4) in (ty3_appl 
+g c2 w u TMP_39 v t TMP_40)))))))))))))) in (let TMP_44 \def (\lambda (c: 
 C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (ty3 g c t3 t4)).(\lambda 
 (H1: ((\forall (c2: C).((wf3 g c c2) \to (ty3 g c2 t3 t4))))).(\lambda (t0: 
 T).(\lambda (_: (ty3 g c t4 t0)).(\lambda (H3: ((\forall (c2: C).((wf3 g c 
 c2) \to (ty3 g c2 t4 t0))))).(\lambda (c2: C).(\lambda (H4: (wf3 g c 
-c2)).(ty3_cast g c2 t3 t4 (H1 c2 H4) t0 (H3 c2 H4)))))))))))) c1 t1 t2 H))))).
-(* COMMENTS
-Initial nodes: 1027
-END *)
+c2)).(let TMP_42 \def (H1 c2 H4) in (let TMP_43 \def (H3 c2 H4) in (ty3_cast 
+g c2 t3 t4 TMP_42 t0 TMP_43))))))))))))) in (ty3_ind g TMP_1 TMP_9 TMP_10 
+TMP_21 TMP_32 TMP_38 TMP_41 TMP_44 c1 t1 t2 H))))))))))))).
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt b/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt
index 817f67b9c92a1772f3160a0763b59ccb7aa03ee0..0ff386374a704bfef93876b4496284119e42130c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/basic_1.txt
@@ -1,3 +1,12 @@
+# new ########################################################################
+
+s_le_gen s_lt_gen
+r_arith2 r_arith3 r_arith4 r_arith5 r_arith6 r_arith7 
+tle tle_r
+cle_r cle_head cle_trans_head cle_flt_trans
+lift_tle lift_free_sym
+subst0_gen_lift_rev_ge
+
 # waiting ####################################################################
 
 aplus/props aplus_reg_r
@@ -240,3 +249,4 @@ wf3/ty3 wf3_pc3_conf
 wf3/ty3 wf3_ty3_conf
 
 # check ######################################################################
+