X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fty3%2Fprops.ma;h=4ffc591adbfe89864d1b6b865fd97e3da615c6d6;hb=e92710b1d9774a6491122668c8463b8658114610;hp=7fbddf8ebfd72f55b0badcc4430a216a18cb22f1;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma
index 7fbddf8eb..4ffc591ad 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+include "LambdaDelta-1/ty3/fwd.ma".
 
-
-include "ty3/fwd.ma".
-
-include "pc3/fwd.ma".
+include "LambdaDelta-1/pc3/fwd.ma".
 
 theorem ty3_lift:
  \forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((ty3 g e 
@@ -135,58 +133,53 @@ nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d u) (lift h d
 t)))))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 
 g (CHead c (Bind b) u) t0 t3)).(\lambda (H3: ((\forall (c0: C).(\forall (d: 
 nat).(\forall (h: nat).((drop h d c0 (CHead c (Bind b) u)) \to (ty3 g c0 
-(lift h d t0) (lift h d t3)))))))).(\lambda (t4: T).(\lambda (_: (ty3 g 
-(CHead c (Bind b) u) t3 t4)).(\lambda (H5: ((\forall (c0: C).(\forall (d: 
-nat).(\forall (h: nat).((drop h d c0 (CHead c (Bind b) u)) \to (ty3 g c0 
-(lift h d t3) (lift h d t4)))))))).(\lambda (c0: C).(\lambda (d: 
-nat).(\lambda (h: nat).(\lambda (H6: (drop h d c0 c)).(eq_ind_r T (THead 
-(Bind b) (lift h d u) (lift h (s (Bind b) d) t0)) (\lambda (t5: T).(ty3 g c0 
-t5 (lift h d (THead (Bind b) u t3)))) (eq_ind_r T (THead (Bind b) (lift h d 
-u) (lift h (s (Bind b) d) t3)) (\lambda (t5: T).(ty3 g c0 (THead (Bind b) 
-(lift h d u) (lift h (s (Bind b) d) t0)) t5)) (ty3_bind g c0 (lift h d u) 
-(lift h d t) (H1 c0 d h H6) b (lift h (S d) t0) (lift h (S d) t3) (H3 (CHead 
-c0 (Bind b) (lift h d u)) (S d) h (drop_skip_bind h d c0 c H6 b u)) (lift h 
-(S d) t4) (H5 (CHead c0 (Bind b) (lift h d u)) (S d) h (drop_skip_bind h d c0 
-c H6 b u))) (lift h d (THead (Bind b) u t3)) (lift_head (Bind b) u t3 h d)) 
-(lift h d (THead (Bind b) u t0)) (lift_head (Bind b) u t0 h 
-d))))))))))))))))))) (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda 
-(_: (ty3 g c w u)).(\lambda (H1: ((\forall (c0: C).(\forall (d: nat).(\forall 
-(h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d w) (lift h d 
-u)))))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead 
-(Bind Abst) u t))).(\lambda (H3: ((\forall (c0: C).(\forall (d: nat).(\forall 
-(h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d v) (lift h d (THead (Bind 
-Abst) u t))))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: 
-nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead (Flat Appl) (lift h d 
-w) (lift h (s (Flat Appl) d) v)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d 
-(THead (Flat Appl) w (THead (Bind Abst) u t))))) (eq_ind_r T (THead (Flat 
-Appl) (lift h d w) (lift h (s (Flat Appl) d) (THead (Bind Abst) u t))) 
-(\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) (lift h d w) (lift h (s (Flat 
-Appl) d) v)) t0)) (eq_ind_r T (THead (Bind Abst) (lift h (s (Flat Appl) d) u) 
-(lift h (s (Bind Abst) (s (Flat Appl) d)) t)) (\lambda (t0: T).(ty3 g c0 
-(THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v)) (THead (Flat 
-Appl) (lift h d w) t0))) (ty3_appl g c0 (lift h d w) (lift h d u) (H1 c0 d h 
-H4) (lift h d v) (lift h (S d) t) (eq_ind T (lift h d (THead (Bind Abst) u 
-t)) (\lambda (t0: T).(ty3 g c0 (lift h d v) t0)) (H3 c0 d h H4) (THead (Bind 
-Abst) (lift h d u) (lift h (S d) t)) (lift_bind Abst u t h d))) (lift h (s 
-(Flat Appl) d) (THead (Bind Abst) u t)) (lift_head (Bind Abst) u t h (s (Flat 
-Appl) d))) (lift h d (THead (Flat Appl) w (THead (Bind Abst) u t))) 
-(lift_head (Flat Appl) w (THead (Bind Abst) u t) h d)) (lift h d (THead (Flat 
-Appl) w v)) (lift_head (Flat Appl) w v h d))))))))))))))) (\lambda (c: 
-C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 g c t0 t3)).(\lambda 
-(H1: ((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) 
-\to (ty3 g c0 (lift h d t0) (lift h d t3)))))))).(\lambda (t4: T).(\lambda 
-(_: (ty3 g c t3 t4)).(\lambda (H3: ((\forall (c0: C).(\forall (d: 
-nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d t3) (lift h d 
-t4)))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H4: 
-(drop h d c0 c)).(eq_ind_r T (THead (Flat Cast) (lift h d t3) (lift h (s 
-(Flat Cast) d) t0)) (\lambda (t: T).(ty3 g c0 t (lift h d (THead (Flat Cast) 
-t4 t3)))) (eq_ind_r T (THead (Flat Cast) (lift h d t4) (lift h (s (Flat Cast) 
-d) t3)) (\lambda (t: T).(ty3 g c0 (THead (Flat Cast) (lift h d t3) (lift h (s 
-(Flat Cast) d) t0)) t)) (ty3_cast g c0 (lift h (s (Flat Cast) d) t0) (lift h 
-(s (Flat Cast) d) t3) (H1 c0 (s (Flat Cast) d) h H4) (lift h d t4) (H3 c0 d h 
-H4)) (lift h d (THead (Flat Cast) t4 t3)) (lift_head (Flat Cast) t4 t3 h d)) 
-(lift h d (THead (Flat Cast) t3 t0)) (lift_head (Flat Cast) t3 t0 h 
-d)))))))))))))) e t1 t2 H))))).
+(lift h d t0) (lift h d t3)))))))).(\lambda (c0: C).(\lambda (d: 
+nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead 
+(Bind b) (lift h d u) (lift h (s (Bind b) d) t0)) (\lambda (t4: T).(ty3 g c0 
+t4 (lift h d (THead (Bind b) u t3)))) (eq_ind_r T (THead (Bind b) (lift h d 
+u) (lift h (s (Bind b) d) t3)) (\lambda (t4: T).(ty3 g c0 (THead (Bind b) 
+(lift h d u) (lift h (s (Bind b) d) t0)) t4)) (ty3_bind g c0 (lift h d u) 
+(lift h d t) (H1 c0 d h H4) b (lift h (S d) t0) (lift h (S d) t3) (H3 (CHead 
+c0 (Bind b) (lift h d u)) (S d) h (drop_skip_bind h d c0 c H4 b u))) (lift h 
+d (THead (Bind b) u t3)) (lift_head (Bind b) u t3 h d)) (lift h d (THead 
+(Bind b) u t0)) (lift_head (Bind b) u t0 h d)))))))))))))))) (\lambda (c: 
+C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c w u)).(\lambda (H1: 
+((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to 
+(ty3 g c0 (lift h d w) (lift h d u)))))))).(\lambda (v: T).(\lambda (t: 
+T).(\lambda (_: (ty3 g c v (THead (Bind Abst) u t))).(\lambda (H3: ((\forall 
+(c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 
+(lift h d v) (lift h d (THead (Bind Abst) u t))))))))).(\lambda (c0: 
+C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0 
+c)).(eq_ind_r T (THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v)) 
+(\lambda (t0: T).(ty3 g c0 t0 (lift h d (THead (Flat Appl) w (THead (Bind 
+Abst) u t))))) (eq_ind_r T (THead (Flat Appl) (lift h d w) (lift h (s (Flat 
+Appl) d) (THead (Bind Abst) u t))) (\lambda (t0: T).(ty3 g c0 (THead (Flat 
+Appl) (lift h d w) (lift h (s (Flat Appl) d) v)) t0)) (eq_ind_r T (THead 
+(Bind Abst) (lift h (s (Flat Appl) d) u) (lift h (s (Bind Abst) (s (Flat 
+Appl) d)) t)) (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) (lift h d w) 
+(lift h (s (Flat Appl) d) v)) (THead (Flat Appl) (lift h d w) t0))) (ty3_appl 
+g c0 (lift h d w) (lift h d u) (H1 c0 d h H4) (lift h d v) (lift h (S d) t) 
+(eq_ind T (lift h d (THead (Bind Abst) u t)) (\lambda (t0: T).(ty3 g c0 (lift 
+h d v) t0)) (H3 c0 d h H4) (THead (Bind Abst) (lift h d u) (lift h (S d) t)) 
+(lift_bind Abst u t h d))) (lift h (s (Flat Appl) d) (THead (Bind Abst) u t)) 
+(lift_head (Bind Abst) u t h (s (Flat Appl) d))) (lift h d (THead (Flat Appl) 
+w (THead (Bind Abst) u t))) (lift_head (Flat Appl) w (THead (Bind Abst) u t) 
+h d)) (lift h d (THead (Flat Appl) w v)) (lift_head (Flat Appl) w v h 
+d))))))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (t3: T).(\lambda 
+(_: (ty3 g c t0 t3)).(\lambda (H1: ((\forall (c0: C).(\forall (d: 
+nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d t0) (lift h d 
+t3)))))))).(\lambda (t4: T).(\lambda (_: (ty3 g c t3 t4)).(\lambda (H3: 
+((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to 
+(ty3 g c0 (lift h d t3) (lift h d t4)))))))).(\lambda (c0: C).(\lambda (d: 
+nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead 
+(Flat Cast) (lift h d t3) (lift h (s (Flat Cast) d) t0)) (\lambda (t: T).(ty3 
+g c0 t (lift h d (THead (Flat Cast) t4 t3)))) (eq_ind_r T (THead (Flat Cast) 
+(lift h d t4) (lift h (s (Flat Cast) d) t3)) (\lambda (t: T).(ty3 g c0 (THead 
+(Flat Cast) (lift h d t3) (lift h (s (Flat Cast) d) t0)) t)) (ty3_cast g c0 
+(lift h (s (Flat Cast) d) t0) (lift h (s (Flat Cast) d) t3) (H1 c0 (s (Flat 
+Cast) d) h H4) (lift h d t4) (H3 c0 d h H4)) (lift h d (THead (Flat Cast) t4 
+t3)) (lift_head (Flat Cast) t4 t3 h d)) (lift h d (THead (Flat Cast) t3 t0)) 
+(lift_head (Flat Cast) t3 t0 h d)))))))))))))) e t1 t2 H))))).
 
 theorem ty3_correct:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c 
@@ -216,46 +209,40 @@ Abst) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (_: (ex T
 (getl_drop Abst c0 d u n H0))))))))))) (\lambda (c0: C).(\lambda (u: 
 T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 u t)).(\lambda (_: (ex T (\lambda 
 (t0: T).(ty3 g c0 t t0)))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3: 
-T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t0 t3)).(\lambda (_: (ex T 
-(\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)))).(\lambda (t4: 
-T).(\lambda (H4: (ty3 g (CHead c0 (Bind b) u) t3 t4)).(\lambda (H5: (ex T 
-(\lambda (t5: T).(ty3 g (CHead c0 (Bind b) u) t4 t5)))).(let H6 \def H5 in 
-(ex_ind T (\lambda (t5: T).(ty3 g (CHead c0 (Bind b) u) t4 t5)) (ex T 
-(\lambda (t5: T).(ty3 g c0 (THead (Bind b) u t3) t5))) (\lambda (x: 
-T).(\lambda (H7: (ty3 g (CHead c0 (Bind b) u) t4 x)).(ex_intro T (\lambda 
-(t5: T).(ty3 g c0 (THead (Bind b) u t3) t5)) (THead (Bind b) u t4) (ty3_bind 
-g c0 u t H0 b t3 t4 H4 x H7)))) H6))))))))))))))) (\lambda (c0: C).(\lambda 
-(w: T).(\lambda (u: T).(\lambda (H0: (ty3 g c0 w u)).(\lambda (H1: (ex T 
-(\lambda (t: T).(ty3 g c0 u t)))).(\lambda (v: T).(\lambda (t: T).(\lambda 
-(_: (ty3 g c0 v (THead (Bind Abst) u t))).(\lambda (H3: (ex T (\lambda (t0: 
-T).(ty3 g c0 (THead (Bind Abst) u t) t0)))).(let H4 \def H1 in (ex_ind T 
-(\lambda (t0: T).(ty3 g c0 u t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead 
-(Flat Appl) w (THead (Bind Abst) u t)) t0))) (\lambda (x: T).(\lambda (_: 
-(ty3 g c0 u x)).(let H6 \def H3 in (ex_ind T (\lambda (t0: T).(ty3 g c0 
-(THead (Bind Abst) u t) t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat 
-Appl) w (THead (Bind Abst) u t)) t0))) (\lambda (x0: T).(\lambda (H7: (ty3 g 
-c0 (THead (Bind Abst) u t) x0)).(ex4_3_ind T T T (\lambda (t3: T).(\lambda 
-(_: T).(\lambda (_: T).(pc3 c0 (THead (Bind Abst) u t3) x0)))) (\lambda (_: 
-T).(\lambda (t0: T).(\lambda (_: T).(ty3 g c0 u t0)))) (\lambda (t3: 
-T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind Abst) u) t t3)))) 
-(\lambda (t3: T).(\lambda (_: T).(\lambda (t4: T).(ty3 g (CHead c0 (Bind 
-Abst) u) t3 t4)))) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w 
-(THead (Bind Abst) u t)) t0))) (\lambda (x1: T).(\lambda (x2: T).(\lambda 
-(x3: T).(\lambda (_: (pc3 c0 (THead (Bind Abst) u x1) x0)).(\lambda (H9: (ty3 
-g c0 u x2)).(\lambda (H10: (ty3 g (CHead c0 (Bind Abst) u) t x1)).(\lambda 
-(H11: (ty3 g (CHead c0 (Bind Abst) u) x1 x3)).(ex_intro T (\lambda (t0: 
-T).(ty3 g c0 (THead (Flat Appl) w (THead (Bind Abst) u t)) t0)) (THead (Flat 
-Appl) w (THead (Bind Abst) u x1)) (ty3_appl g c0 w u H0 (THead (Bind Abst) u 
-t) x1 (ty3_bind g c0 u x2 H9 Abst t x1 H10 x3 H11)))))))))) (ty3_gen_bind g 
-Abst c0 u t x0 H7)))) H6)))) H4))))))))))) (\lambda (c0: C).(\lambda (t0: 
-T).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t0 t3)).(\lambda (_: (ex T 
-(\lambda (t: T).(ty3 g c0 t3 t)))).(\lambda (t4: T).(\lambda (H2: (ty3 g c0 
-t3 t4)).(\lambda (H3: (ex T (\lambda (t: T).(ty3 g c0 t4 t)))).(let H4 \def 
-H3 in (ex_ind T (\lambda (t: T).(ty3 g c0 t4 t)) (ex T (\lambda (t: T).(ty3 g 
-c0 (THead (Flat Cast) t4 t3) t))) (\lambda (x: T).(\lambda (H5: (ty3 g c0 t4 
-x)).(ex_intro T (\lambda (t: T).(ty3 g c0 (THead (Flat Cast) t4 t3) t)) 
-(THead (Flat Cast) x t4) (ty3_cast g c0 t3 t4 H2 x H5)))) H4)))))))))) c t1 
-t2 H))))).
+T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t0 t3)).(\lambda (H3: (ex T 
+(\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)))).(let H4 \def H3 in 
+(ex_ind T (\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)) (ex T 
+(\lambda (t4: T).(ty3 g c0 (THead (Bind b) u t3) t4))) (\lambda (x: 
+T).(\lambda (H5: (ty3 g (CHead c0 (Bind b) u) t3 x)).(ex_intro T (\lambda 
+(t4: T).(ty3 g c0 (THead (Bind b) u t3) t4)) (THead (Bind b) u x) (ty3_bind g 
+c0 u t H0 b t3 x H5)))) H4)))))))))))) (\lambda (c0: C).(\lambda (w: 
+T).(\lambda (u: T).(\lambda (H0: (ty3 g c0 w u)).(\lambda (H1: (ex T (\lambda 
+(t: T).(ty3 g c0 u t)))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g 
+c0 v (THead (Bind Abst) u t))).(\lambda (H3: (ex T (\lambda (t0: T).(ty3 g c0 
+(THead (Bind Abst) u t) t0)))).(let H4 \def H1 in (ex_ind T (\lambda (t0: 
+T).(ty3 g c0 u t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w 
+(THead (Bind Abst) u t)) t0))) (\lambda (x: T).(\lambda (_: (ty3 g c0 u 
+x)).(let H6 \def H3 in (ex_ind T (\lambda (t0: T).(ty3 g c0 (THead (Bind 
+Abst) u t) t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w (THead 
+(Bind Abst) u t)) t0))) (\lambda (x0: T).(\lambda (H7: (ty3 g c0 (THead (Bind 
+Abst) u t) x0)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c0 
+(THead (Bind Abst) u t3) x0))) (\lambda (_: T).(\lambda (t0: T).(ty3 g c0 u 
+t0))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind Abst) u) t 
+t3))) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w (THead (Bind 
+Abst) u t)) t0))) (\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c0 
+(THead (Bind Abst) u x1) x0)).(\lambda (H9: (ty3 g c0 u x2)).(\lambda (H10: 
+(ty3 g (CHead c0 (Bind Abst) u) t x1)).(ex_intro T (\lambda (t0: T).(ty3 g c0 
+(THead (Flat Appl) w (THead (Bind Abst) u t)) t0)) (THead (Flat Appl) w 
+(THead (Bind Abst) u x1)) (ty3_appl g c0 w u H0 (THead (Bind Abst) u t) x1 
+(ty3_bind g c0 u x2 H9 Abst t x1 H10)))))))) (ty3_gen_bind g Abst c0 u t x0 
+H7)))) H6)))) H4))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t3: 
+T).(\lambda (_: (ty3 g c0 t0 t3)).(\lambda (_: (ex T (\lambda (t: T).(ty3 g 
+c0 t3 t)))).(\lambda (t4: T).(\lambda (H2: (ty3 g c0 t3 t4)).(\lambda (H3: 
+(ex T (\lambda (t: T).(ty3 g c0 t4 t)))).(let H4 \def H3 in (ex_ind T 
+(\lambda (t: T).(ty3 g c0 t4 t)) (ex T (\lambda (t: T).(ty3 g c0 (THead (Flat 
+Cast) t4 t3) t))) (\lambda (x: T).(\lambda (H5: (ty3 g c0 t4 x)).(ex_intro T 
+(\lambda (t: T).(ty3 g c0 (THead (Flat Cast) t4 t3) t)) (THead (Flat Cast) x 
+t4) (ty3_cast g c0 t3 t4 H2 x H5)))) H4)))))))))) c t1 t2 H))))).
 
 theorem ty3_unique:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u 
@@ -392,47 +379,42 @@ n H3)))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (t: T).(\lambda
 (pc3 c0 t t2))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t2: T).(\lambda 
 (_: (ty3 g (CHead c0 (Bind b) u0) t0 t2)).(\lambda (H3: ((\forall (t3: 
 T).((ty3 g (CHead c0 (Bind b) u0) t0 t3) \to (pc3 (CHead c0 (Bind b) u0) t2 
-t3))))).(\lambda (t3: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u0) t2 
-t3)).(\lambda (_: ((\forall (t4: T).((ty3 g (CHead c0 (Bind b) u0) t2 t4) \to 
-(pc3 (CHead c0 (Bind b) u0) t3 t4))))).(\lambda (t4: T).(\lambda (H6: (ty3 g 
-c0 (THead (Bind b) u0 t0) t4)).(ex4_3_ind T T T (\lambda (t5: T).(\lambda (_: 
-T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u0 t5) t4)))) (\lambda (_: 
-T).(\lambda (t6: T).(\lambda (_: T).(ty3 g c0 u0 t6)))) (\lambda (t5: 
-T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u0) t0 t5)))) 
-(\lambda (t5: T).(\lambda (_: T).(\lambda (t7: T).(ty3 g (CHead c0 (Bind b) 
-u0) t5 t7)))) (pc3 c0 (THead (Bind b) u0 t2) t4) (\lambda (x0: T).(\lambda 
-(x1: T).(\lambda (x2: T).(\lambda (H7: (pc3 c0 (THead (Bind b) u0 x0) 
-t4)).(\lambda (_: (ty3 g c0 u0 x1)).(\lambda (H9: (ty3 g (CHead c0 (Bind b) 
-u0) t0 x0)).(\lambda (_: (ty3 g (CHead c0 (Bind b) u0) x0 x2)).(pc3_t (THead 
-(Bind b) u0 x0) c0 (THead (Bind b) u0 t2) (pc3_head_2 c0 u0 t2 x0 (Bind b) 
-(H3 x0 H9)) t4 H7)))))))) (ty3_gen_bind g b c0 u0 t0 t4 H6))))))))))))))))) 
-(\lambda (c0: C).(\lambda (w: T).(\lambda (u0: T).(\lambda (_: (ty3 g c0 w 
-u0)).(\lambda (_: ((\forall (t2: T).((ty3 g c0 w t2) \to (pc3 c0 u0 
-t2))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v (THead (Bind 
-Abst) u0 t))).(\lambda (H3: ((\forall (t2: T).((ty3 g c0 v t2) \to (pc3 c0 
-(THead (Bind Abst) u0 t) t2))))).(\lambda (t2: T).(\lambda (H4: (ty3 g c0 
-(THead (Flat Appl) w v) t2)).(ex3_2_ind T T (\lambda (u1: T).(\lambda (t0: 
-T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u1 t0)) t2))) (\lambda 
-(u1: T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u1 t0)))) (\lambda 
-(u1: T).(\lambda (_: T).(ty3 g c0 w u1))) (pc3 c0 (THead (Flat Appl) w (THead 
-(Bind Abst) u0 t)) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (pc3 
-c0 (THead (Flat Appl) w (THead (Bind Abst) x0 x1)) t2)).(\lambda (H6: (ty3 g 
-c0 v (THead (Bind Abst) x0 x1))).(\lambda (_: (ty3 g c0 w x0)).(pc3_t (THead 
-(Flat Appl) w (THead (Bind Abst) x0 x1)) c0 (THead (Flat Appl) w (THead (Bind 
-Abst) u0 t)) (pc3_thin_dx c0 (THead (Bind Abst) u0 t) (THead (Bind Abst) x0 
-x1) (H3 (THead (Bind Abst) x0 x1) H6) w Appl) t2 H5)))))) (ty3_gen_appl g c0 
-w v t2 H4))))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t2: 
-T).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (_: ((\forall (t3: T).((ty3 g c0 
-t0 t3) \to (pc3 c0 t2 t3))))).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t2 
-t3)).(\lambda (H3: ((\forall (t4: T).((ty3 g c0 t2 t4) \to (pc3 c0 t3 
-t4))))).(\lambda (t4: T).(\lambda (H4: (ty3 g c0 (THead (Flat Cast) t2 t0) 
-t4)).(ex3_ind T (\lambda (t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) t4)) 
-(\lambda (_: T).(ty3 g c0 t0 t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)) (pc3 c0 
-(THead (Flat Cast) t3 t2) t4) (\lambda (x0: T).(\lambda (H5: (pc3 c0 (THead 
-(Flat Cast) x0 t2) t4)).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (H7: (ty3 g 
-c0 t2 x0)).(pc3_t (THead (Flat Cast) x0 t2) c0 (THead (Flat Cast) t3 t2) 
-(pc3_head_1 c0 t3 x0 (H3 x0 H7) (Flat Cast) t2) t4 H5))))) (ty3_gen_cast g c0 
-t0 t2 t4 H4)))))))))))) c u t1 H))))).
+t3))))).(\lambda (t3: T).(\lambda (H4: (ty3 g c0 (THead (Bind b) u0 t0) 
+t3)).(ex3_2_ind T T (\lambda (t4: T).(\lambda (_: T).(pc3 c0 (THead (Bind b) 
+u0 t4) t3))) (\lambda (_: T).(\lambda (t5: T).(ty3 g c0 u0 t5))) (\lambda 
+(t4: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind b) u0) t0 t4))) (pc3 c0 (THead 
+(Bind b) u0 t2) t3) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (pc3 c0 
+(THead (Bind b) u0 x0) t3)).(\lambda (_: (ty3 g c0 u0 x1)).(\lambda (H7: (ty3 
+g (CHead c0 (Bind b) u0) t0 x0)).(pc3_t (THead (Bind b) u0 x0) c0 (THead 
+(Bind b) u0 t2) (pc3_head_2 c0 u0 t2 x0 (Bind b) (H3 x0 H7)) t3 H5)))))) 
+(ty3_gen_bind g b c0 u0 t0 t3 H4)))))))))))))) (\lambda (c0: C).(\lambda (w: 
+T).(\lambda (u0: T).(\lambda (_: (ty3 g c0 w u0)).(\lambda (_: ((\forall (t2: 
+T).((ty3 g c0 w t2) \to (pc3 c0 u0 t2))))).(\lambda (v: T).(\lambda (t: 
+T).(\lambda (_: (ty3 g c0 v (THead (Bind Abst) u0 t))).(\lambda (H3: 
+((\forall (t2: T).((ty3 g c0 v t2) \to (pc3 c0 (THead (Bind Abst) u0 t) 
+t2))))).(\lambda (t2: T).(\lambda (H4: (ty3 g c0 (THead (Flat Appl) w v) 
+t2)).(ex3_2_ind T T (\lambda (u1: T).(\lambda (t0: T).(pc3 c0 (THead (Flat 
+Appl) w (THead (Bind Abst) u1 t0)) t2))) (\lambda (u1: T).(\lambda (t0: 
+T).(ty3 g c0 v (THead (Bind Abst) u1 t0)))) (\lambda (u1: T).(\lambda (_: 
+T).(ty3 g c0 w u1))) (pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t)) 
+t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (pc3 c0 (THead (Flat 
+Appl) w (THead (Bind Abst) x0 x1)) t2)).(\lambda (H6: (ty3 g c0 v (THead 
+(Bind Abst) x0 x1))).(\lambda (_: (ty3 g c0 w x0)).(pc3_t (THead (Flat Appl) 
+w (THead (Bind Abst) x0 x1)) c0 (THead (Flat Appl) w (THead (Bind Abst) u0 
+t)) (pc3_thin_dx c0 (THead (Bind Abst) u0 t) (THead (Bind Abst) x0 x1) (H3 
+(THead (Bind Abst) x0 x1) H6) w Appl) t2 H5)))))) (ty3_gen_appl g c0 w v t2 
+H4))))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t2: T).(\lambda 
+(_: (ty3 g c0 t0 t2)).(\lambda (_: ((\forall (t3: T).((ty3 g c0 t0 t3) \to 
+(pc3 c0 t2 t3))))).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t2 t3)).(\lambda 
+(H3: ((\forall (t4: T).((ty3 g c0 t2 t4) \to (pc3 c0 t3 t4))))).(\lambda (t4: 
+T).(\lambda (H4: (ty3 g c0 (THead (Flat Cast) t2 t0) t4)).(ex3_ind T (\lambda 
+(t5: T).(pc3 c0 (THead (Flat Cast) t5 t2) t4)) (\lambda (_: T).(ty3 g c0 t0 
+t2)) (\lambda (t5: T).(ty3 g c0 t2 t5)) (pc3 c0 (THead (Flat Cast) t3 t2) t4) 
+(\lambda (x0: T).(\lambda (H5: (pc3 c0 (THead (Flat Cast) x0 t2) 
+t4)).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (H7: (ty3 g c0 t2 x0)).(pc3_t 
+(THead (Flat Cast) x0 t2) c0 (THead (Flat Cast) t3 t2) (pc3_head_1 c0 t3 x0 
+(H3 x0 H7) (Flat Cast) t2) t4 H5))))) (ty3_gen_cast g c0 t0 t2 t4 
+H4)))))))))))) c u t1 H))))).
 
 theorem ty3_gen_abst_abst:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall 
@@ -445,30 +427,25 @@ u) t1 t2))))))))
 t2))).(ex_ind T (\lambda (t: T).(ty3 g c (THead (Bind Abst) u t2) t)) (ex2 T 
 (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) 
 t1 t2))) (\lambda (x: T).(\lambda (H0: (ty3 g c (THead (Bind Abst) u t2) 
-x)).(ex4_3_ind T T T (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(pc3 c 
-(THead (Bind Abst) u t3) x)))) (\lambda (_: T).(\lambda (t: T).(\lambda (_: 
-T).(ty3 g c u t)))) (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(ty3 g 
-(CHead c (Bind Abst) u) t2 t3)))) (\lambda (t3: T).(\lambda (_: T).(\lambda 
-(t0: T).(ty3 g (CHead c (Bind Abst) u) t3 t0)))) (ex2 T (\lambda (w: T).(ty3 
-g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2))) (\lambda 
-(x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c (THead (Bind 
-Abst) u x0) x)).(\lambda (H2: (ty3 g c u x1)).(\lambda (H3: (ty3 g (CHead c 
-(Bind Abst) u) t2 x0)).(\lambda (_: (ty3 g (CHead c (Bind Abst) u) x0 
-x2)).(ex4_3_ind T T T (\lambda (t3: T).(\lambda (_: T).(\lambda (_: T).(pc3 c 
-(THead (Bind Abst) u t3) (THead (Bind Abst) u t2))))) (\lambda (_: 
-T).(\lambda (t: T).(\lambda (_: T).(ty3 g c u t)))) (\lambda (t3: T).(\lambda 
-(_: T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t3)))) (\lambda (t3: 
-T).(\lambda (_: T).(\lambda (t0: T).(ty3 g (CHead c (Bind Abst) u) t3 t0)))) 
-(ex2 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind 
-Abst) u) t1 t2))) (\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda 
-(H5: (pc3 c (THead (Bind Abst) u x3) (THead (Bind Abst) u t2))).(\lambda (_: 
-(ty3 g c u x4)).(\lambda (H7: (ty3 g (CHead c (Bind Abst) u) t1 x3)).(\lambda 
-(_: (ty3 g (CHead c (Bind Abst) u) x3 x5)).(let H_y \def (pc3_gen_abst_shift 
-c u x3 t2 H5) in (ex_intro2 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_: 
-T).(ty3 g (CHead c (Bind Abst) u) t1 t2)) x1 H2 (ty3_conv g (CHead c (Bind 
-Abst) u) t2 x0 H3 t1 x3 H7 H_y)))))))))) (ty3_gen_bind g Abst c u t1 (THead 
-(Bind Abst) u t2) H))))))))) (ty3_gen_bind g Abst c u t2 x H0)))) 
-(ty3_correct g c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2) H))))))).
+x)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c (THead (Bind Abst) 
+u t3) x))) (\lambda (_: T).(\lambda (t: T).(ty3 g c u t))) (\lambda (t3: 
+T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t2 t3))) (ex2 T (\lambda 
+(w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2))) 
+(\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (pc3 c (THead (Bind Abst) u 
+x0) x)).(\lambda (_: (ty3 g c u x1)).(\lambda (H3: (ty3 g (CHead c (Bind 
+Abst) u) t2 x0)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c 
+(THead (Bind Abst) u t3) (THead (Bind Abst) u t2)))) (\lambda (_: T).(\lambda 
+(t: T).(ty3 g c u t))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c (Bind 
+Abst) u) t1 t3))) (ex2 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 
+g (CHead c (Bind Abst) u) t1 t2))) (\lambda (x2: T).(\lambda (x3: T).(\lambda 
+(H4: (pc3 c (THead (Bind Abst) u x2) (THead (Bind Abst) u t2))).(\lambda (H5: 
+(ty3 g c u x3)).(\lambda (H6: (ty3 g (CHead c (Bind Abst) u) t1 x2)).(let H_y 
+\def (pc3_gen_abst_shift c u x2 t2 H4) in (ex_intro2 T (\lambda (w: T).(ty3 g 
+c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2)) x3 H5 
+(ty3_conv g (CHead c (Bind Abst) u) t2 x0 H3 t1 x2 H6 H_y)))))))) 
+(ty3_gen_bind g Abst c u t1 (THead (Bind Abst) u t2) H))))))) (ty3_gen_bind g 
+Abst c u t2 x H0)))) (ty3_correct g c (THead (Bind Abst) u t1) (THead (Bind 
+Abst) u t2) H))))))).
 
 theorem ty3_typecheck:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (v: T).((ty3 g c t