X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fty3%2Ftau0.ma;h=ceaa58478d16de7f555a26b1e678649f0db4c46a;hb=e92710b1d9774a6491122668c8463b8658114610;hp=a9fb878eae4b678e73d93e0b15b8a692c9296d5d;hpb=81cb773cbc402fc74752fb69a436b25be49489ee;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma
index a9fb878ea..ceaa58478 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0".
+include "LambdaDelta-1/ty3/pr3_props.ma".
 
-include "ty3/pr3_props.ma".
-
-include "tau0/defs.ma".
+include "LambdaDelta-1/tau0/defs.ma".
 
 theorem ty3_tau0:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u 
@@ -312,127 +310,121 @@ C).(\lambda (u0: T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 u0 t)).(\lambda
 (b: B).(\lambda (t2: T).(\lambda (t3: T).(\lambda (_: (ty3 g (CHead c0 (Bind 
 b) u0) t2 t3)).(\lambda (H3: ((\forall (t4: T).((tau0 g (CHead c0 (Bind b) 
 u0) t2 t4) \to (ty3 g (CHead c0 (Bind b) u0) t2 t4))))).(\lambda (t0: 
-T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u0) t3 t0)).(\lambda (_: ((\forall 
-(t4: T).((tau0 g (CHead c0 (Bind b) u0) t3 t4) \to (ty3 g (CHead c0 (Bind b) 
-u0) t3 t4))))).(\lambda (t4: T).(\lambda (H6: (tau0 g c0 (THead (Bind b) u0 
-t2) t4)).(let H7 \def (match H6 in tau0 return (\lambda (c1: C).(\lambda (t5: 
-T).(\lambda (t6: T).(\lambda (_: (tau0 ? c1 t5 t6)).((eq C c1 c0) \to ((eq T 
-t5 (THead (Bind b) u0 t2)) \to ((eq T t6 t4) \to (ty3 g c0 (THead (Bind b) u0 
-t2) t4)))))))) with [(tau0_sort c1 n) \Rightarrow (\lambda (H7: (eq C c1 
-c0)).(\lambda (H8: (eq T (TSort n) (THead (Bind b) u0 t2))).(\lambda (H9: (eq 
-T (TSort (next g n)) t4)).(eq_ind C c0 (\lambda (_: C).((eq T (TSort n) 
-(THead (Bind b) u0 t2)) \to ((eq T (TSort (next g n)) t4) \to (ty3 g c0 
-(THead (Bind b) u0 t2) t4)))) (\lambda (H10: (eq T (TSort n) (THead (Bind b) 
-u0 t2))).(let H11 \def (eq_ind T (TSort n) (\lambda (e: T).(match e in T 
-return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) 
-\Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Bind b) u0 
-t2) H10) in (False_ind ((eq T (TSort (next g n)) t4) \to (ty3 g c0 (THead 
-(Bind b) u0 t2) t4)) H11))) c1 (sym_eq C c1 c0 H7) H8 H9)))) | (tau0_abbr c1 
-d v i H7 w H8) \Rightarrow (\lambda (H9: (eq C c1 c0)).(\lambda (H10: (eq T 
-(TLRef i) (THead (Bind b) u0 t2))).(\lambda (H11: (eq T (lift (S i) O w) 
-t4)).(eq_ind C c0 (\lambda (c2: C).((eq T (TLRef i) (THead (Bind b) u0 t2)) 
-\to ((eq T (lift (S i) O w) t4) \to ((getl i c2 (CHead d (Bind Abbr) v)) \to 
-((tau0 g d v w) \to (ty3 g c0 (THead (Bind b) u0 t2) t4)))))) (\lambda (H12: 
-(eq T (TLRef i) (THead (Bind b) u0 t2))).(let H13 \def (eq_ind T (TLRef i) 
-(\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) 
-\Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow 
-False])) I (THead (Bind b) u0 t2) H12) in (False_ind ((eq T (lift (S i) O w) 
-t4) \to ((getl i c0 (CHead d (Bind Abbr) v)) \to ((tau0 g d v w) \to (ty3 g 
-c0 (THead (Bind b) u0 t2) t4)))) H13))) c1 (sym_eq C c1 c0 H9) H10 H11 H7 
-H8)))) | (tau0_abst c1 d v i H7 w H8) \Rightarrow (\lambda (H9: (eq C c1 
-c0)).(\lambda (H10: (eq T (TLRef i) (THead (Bind b) u0 t2))).(\lambda (H11: 
-(eq T (lift (S i) O v) t4)).(eq_ind C c0 (\lambda (c2: C).((eq T (TLRef i) 
-(THead (Bind b) u0 t2)) \to ((eq T (lift (S i) O v) t4) \to ((getl i c2 
-(CHead d (Bind Abst) v)) \to ((tau0 g d v w) \to (ty3 g c0 (THead (Bind b) u0 
-t2) t4)))))) (\lambda (H12: (eq T (TLRef i) (THead (Bind b) u0 t2))).(let H13 
+T).(\lambda (H4: (tau0 g c0 (THead (Bind b) u0 t2) t0)).(let H5 \def (match 
+H4 in tau0 return (\lambda (c1: C).(\lambda (t4: T).(\lambda (t5: T).(\lambda 
+(_: (tau0 ? c1 t4 t5)).((eq C c1 c0) \to ((eq T t4 (THead (Bind b) u0 t2)) 
+\to ((eq T t5 t0) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)))))))) with 
+[(tau0_sort c1 n) \Rightarrow (\lambda (H5: (eq C c1 c0)).(\lambda (H6: (eq T 
+(TSort n) (THead (Bind b) u0 t2))).(\lambda (H7: (eq T (TSort (next g n)) 
+t0)).(eq_ind C c0 (\lambda (_: C).((eq T (TSort n) (THead (Bind b) u0 t2)) 
+\to ((eq T (TSort (next g n)) t0) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)))) 
+(\lambda (H8: (eq T (TSort n) (THead (Bind b) u0 t2))).(let H9 \def (eq_ind T 
+(TSort n) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with 
+[(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) 
+\Rightarrow False])) I (THead (Bind b) u0 t2) H8) in (False_ind ((eq T (TSort 
+(next g n)) t0) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)) H9))) c1 (sym_eq C 
+c1 c0 H5) H6 H7)))) | (tau0_abbr c1 d v i H5 w H6) \Rightarrow (\lambda (H7: 
+(eq C c1 c0)).(\lambda (H8: (eq T (TLRef i) (THead (Bind b) u0 t2))).(\lambda 
+(H9: (eq T (lift (S i) O w) t0)).(eq_ind C c0 (\lambda (c2: C).((eq T (TLRef 
+i) (THead (Bind b) u0 t2)) \to ((eq T (lift (S i) O w) t0) \to ((getl i c2 
+(CHead d (Bind Abbr) v)) \to ((tau0 g d v w) \to (ty3 g c0 (THead (Bind b) u0 
+t2) t0)))))) (\lambda (H10: (eq T (TLRef i) (THead (Bind b) u0 t2))).(let H11 
 \def (eq_ind T (TLRef i) (\lambda (e: T).(match e in T return (\lambda (_: 
 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | 
-(THead _ _ _) \Rightarrow False])) I (THead (Bind b) u0 t2) H12) in 
-(False_ind ((eq T (lift (S i) O v) t4) \to ((getl i c0 (CHead d (Bind Abst) 
-v)) \to ((tau0 g d v w) \to (ty3 g c0 (THead (Bind b) u0 t2) t4)))) H13))) c1 
-(sym_eq C c1 c0 H9) H10 H11 H7 H8)))) | (tau0_bind b0 c1 v t5 t6 H7) 
-\Rightarrow (\lambda (H8: (eq C c1 c0)).(\lambda (H9: (eq T (THead (Bind b0) 
-v t5) (THead (Bind b) u0 t2))).(\lambda (H10: (eq T (THead (Bind b0) v t6) 
-t4)).(eq_ind C c0 (\lambda (c2: C).((eq T (THead (Bind b0) v t5) (THead (Bind 
-b) u0 t2)) \to ((eq T (THead (Bind b0) v t6) t4) \to ((tau0 g (CHead c2 (Bind 
-b0) v) t5 t6) \to (ty3 g c0 (THead (Bind b) u0 t2) t4))))) (\lambda (H11: (eq 
-T (THead (Bind b0) v t5) (THead (Bind b) u0 t2))).(let H12 \def (f_equal T T 
-(\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
-\Rightarrow t5 | (TLRef _) \Rightarrow t5 | (THead _ _ t7) \Rightarrow t7])) 
-(THead (Bind b0) v t5) (THead (Bind b) u0 t2) H11) in ((let H13 \def (f_equal 
-T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) 
-\Rightarrow v | (TLRef _) \Rightarrow v | (THead _ t7 _) \Rightarrow t7])) 
-(THead (Bind b0) v t5) (THead (Bind b) u0 t2) H11) in ((let H14 \def (f_equal 
-T B (\lambda (e: T).(match e in T return (\lambda (_: T).B) with [(TSort _) 
-\Rightarrow b0 | (TLRef _) \Rightarrow b0 | (THead k _ _) \Rightarrow (match 
-k in K return (\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | (Flat _) 
-\Rightarrow b0])])) (THead (Bind b0) v t5) (THead (Bind b) u0 t2) H11) in 
-(eq_ind B b (\lambda (b1: B).((eq T v u0) \to ((eq T t5 t2) \to ((eq T (THead 
-(Bind b1) v t6) t4) \to ((tau0 g (CHead c0 (Bind b1) v) t5 t6) \to (ty3 g c0 
-(THead (Bind b) u0 t2) t4)))))) (\lambda (H15: (eq T v u0)).(eq_ind T u0 
-(\lambda (t7: T).((eq T t5 t2) \to ((eq T (THead (Bind b) t7 t6) t4) \to 
-((tau0 g (CHead c0 (Bind b) t7) t5 t6) \to (ty3 g c0 (THead (Bind b) u0 t2) 
-t4))))) (\lambda (H16: (eq T t5 t2)).(eq_ind T t2 (\lambda (t7: T).((eq T 
-(THead (Bind b) u0 t6) t4) \to ((tau0 g (CHead c0 (Bind b) u0) t7 t6) \to 
-(ty3 g c0 (THead (Bind b) u0 t2) t4)))) (\lambda (H17: (eq T (THead (Bind b) 
-u0 t6) t4)).(eq_ind T (THead (Bind b) u0 t6) (\lambda (t7: T).((tau0 g (CHead 
-c0 (Bind b) u0) t2 t6) \to (ty3 g c0 (THead (Bind b) u0 t2) t7))) (\lambda 
-(H18: (tau0 g (CHead c0 (Bind b) u0) t2 t6)).(let H_y \def (H3 t6 H18) in 
-(ex_ind T (\lambda (t7: T).(ty3 g (CHead c0 (Bind b) u0) t6 t7)) (ty3 g c0 
-(THead (Bind b) u0 t2) (THead (Bind b) u0 t6)) (\lambda (x: T).(\lambda (H19: 
-(ty3 g (CHead c0 (Bind b) u0) t6 x)).(ty3_bind g c0 u0 t H0 b t2 t6 H_y x 
-H19))) (ty3_correct g (CHead c0 (Bind b) u0) t2 t6 H_y)))) t4 H17)) t5 
-(sym_eq T t5 t2 H16))) v (sym_eq T v u0 H15))) b0 (sym_eq B b0 b H14))) H13)) 
-H12))) c1 (sym_eq C c1 c0 H8) H9 H10 H7)))) | (tau0_appl c1 v t5 t6 H7) 
-\Rightarrow (\lambda (H8: (eq C c1 c0)).(\lambda (H9: (eq T (THead (Flat 
-Appl) v t5) (THead (Bind b) u0 t2))).(\lambda (H10: (eq T (THead (Flat Appl) 
-v t6) t4)).(eq_ind C c0 (\lambda (c2: C).((eq T (THead (Flat Appl) v t5) 
-(THead (Bind b) u0 t2)) \to ((eq T (THead (Flat Appl) v t6) t4) \to ((tau0 g 
-c2 t5 t6) \to (ty3 g c0 (THead (Bind b) u0 t2) t4))))) (\lambda (H11: (eq T 
-(THead (Flat Appl) v t5) (THead (Bind b) u0 t2))).(let H12 \def (eq_ind T 
-(THead (Flat Appl) v t5) (\lambda (e: T).(match e in T return (\lambda (_: 
+(THead _ _ _) \Rightarrow False])) I (THead (Bind b) u0 t2) H10) in 
+(False_ind ((eq T (lift (S i) O w) t0) \to ((getl i c0 (CHead d (Bind Abbr) 
+v)) \to ((tau0 g d v w) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)))) H11))) c1 
+(sym_eq C c1 c0 H7) H8 H9 H5 H6)))) | (tau0_abst c1 d v i H5 w H6) 
+\Rightarrow (\lambda (H7: (eq C c1 c0)).(\lambda (H8: (eq T (TLRef i) (THead 
+(Bind b) u0 t2))).(\lambda (H9: (eq T (lift (S i) O v) t0)).(eq_ind C c0 
+(\lambda (c2: C).((eq T (TLRef i) (THead (Bind b) u0 t2)) \to ((eq T (lift (S 
+i) O v) t0) \to ((getl i c2 (CHead d (Bind Abst) v)) \to ((tau0 g d v w) \to 
+(ty3 g c0 (THead (Bind b) u0 t2) t0)))))) (\lambda (H10: (eq T (TLRef i) 
+(THead (Bind b) u0 t2))).(let H11 \def (eq_ind T (TLRef i) (\lambda (e: 
+T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
+False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I 
+(THead (Bind b) u0 t2) H10) in (False_ind ((eq T (lift (S i) O v) t0) \to 
+((getl i c0 (CHead d (Bind Abst) v)) \to ((tau0 g d v w) \to (ty3 g c0 (THead 
+(Bind b) u0 t2) t0)))) H11))) c1 (sym_eq C c1 c0 H7) H8 H9 H5 H6)))) | 
+(tau0_bind b0 c1 v t4 t5 H5) \Rightarrow (\lambda (H6: (eq C c1 c0)).(\lambda 
+(H7: (eq T (THead (Bind b0) v t4) (THead (Bind b) u0 t2))).(\lambda (H8: (eq 
+T (THead (Bind b0) v t5) t0)).(eq_ind C c0 (\lambda (c2: C).((eq T (THead 
+(Bind b0) v t4) (THead (Bind b) u0 t2)) \to ((eq T (THead (Bind b0) v t5) t0) 
+\to ((tau0 g (CHead c2 (Bind b0) v) t4 t5) \to (ty3 g c0 (THead (Bind b) u0 
+t2) t0))))) (\lambda (H9: (eq T (THead (Bind b0) v t4) (THead (Bind b) u0 
+t2))).(let H10 \def (f_equal T T (\lambda (e: T).(match e in T return 
+(\lambda (_: T).T) with [(TSort _) \Rightarrow t4 | (TLRef _) \Rightarrow t4 
+| (THead _ _ t6) \Rightarrow t6])) (THead (Bind b0) v t4) (THead (Bind b) u0 
+t2) H9) in ((let H11 \def (f_equal T T (\lambda (e: T).(match e in T return 
+(\lambda (_: T).T) with [(TSort _) \Rightarrow v | (TLRef _) \Rightarrow v | 
+(THead _ t6 _) \Rightarrow t6])) (THead (Bind b0) v t4) (THead (Bind b) u0 
+t2) H9) in ((let H12 \def (f_equal T B (\lambda (e: T).(match e in T return 
+(\lambda (_: T).B) with [(TSort _) \Rightarrow b0 | (TLRef _) \Rightarrow b0 
+| (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).B) with 
+[(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b0])])) (THead (Bind b0) v 
+t4) (THead (Bind b) u0 t2) H9) in (eq_ind B b (\lambda (b1: B).((eq T v u0) 
+\to ((eq T t4 t2) \to ((eq T (THead (Bind b1) v t5) t0) \to ((tau0 g (CHead 
+c0 (Bind b1) v) t4 t5) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)))))) (\lambda 
+(H13: (eq T v u0)).(eq_ind T u0 (\lambda (t6: T).((eq T t4 t2) \to ((eq T 
+(THead (Bind b) t6 t5) t0) \to ((tau0 g (CHead c0 (Bind b) t6) t4 t5) \to 
+(ty3 g c0 (THead (Bind b) u0 t2) t0))))) (\lambda (H14: (eq T t4 t2)).(eq_ind 
+T t2 (\lambda (t6: T).((eq T (THead (Bind b) u0 t5) t0) \to ((tau0 g (CHead 
+c0 (Bind b) u0) t6 t5) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)))) (\lambda 
+(H15: (eq T (THead (Bind b) u0 t5) t0)).(eq_ind T (THead (Bind b) u0 t5) 
+(\lambda (t6: T).((tau0 g (CHead c0 (Bind b) u0) t2 t5) \to (ty3 g c0 (THead 
+(Bind b) u0 t2) t6))) (\lambda (H16: (tau0 g (CHead c0 (Bind b) u0) t2 
+t5)).(ty3_bind g c0 u0 t H0 b t2 t5 (H3 t5 H16))) t0 H15)) t4 (sym_eq T t4 t2 
+H14))) v (sym_eq T v u0 H13))) b0 (sym_eq B b0 b H12))) H11)) H10))) c1 
+(sym_eq C c1 c0 H6) H7 H8 H5)))) | (tau0_appl c1 v t4 t5 H5) \Rightarrow 
+(\lambda (H6: (eq C c1 c0)).(\lambda (H7: (eq T (THead (Flat Appl) v t4) 
+(THead (Bind b) u0 t2))).(\lambda (H8: (eq T (THead (Flat Appl) v t5) 
+t0)).(eq_ind C c0 (\lambda (c2: C).((eq T (THead (Flat Appl) v t4) (THead 
+(Bind b) u0 t2)) \to ((eq T (THead (Flat Appl) v t5) t0) \to ((tau0 g c2 t4 
+t5) \to (ty3 g c0 (THead (Bind b) u0 t2) t0))))) (\lambda (H9: (eq T (THead 
+(Flat Appl) v t4) (THead (Bind b) u0 t2))).(let H10 \def (eq_ind T (THead 
+(Flat Appl) v t4) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) 
+with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ 
+_) \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) 
+\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind b) u0 t2) 
+H9) in (False_ind ((eq T (THead (Flat Appl) v t5) t0) \to ((tau0 g c0 t4 t5) 
+\to (ty3 g c0 (THead (Bind b) u0 t2) t0))) H10))) c1 (sym_eq C c1 c0 H6) H7 
+H8 H5)))) | (tau0_cast c1 v1 v2 H5 t4 t5 H6) \Rightarrow (\lambda (H7: (eq C 
+c1 c0)).(\lambda (H8: (eq T (THead (Flat Cast) v1 t4) (THead (Bind b) u0 
+t2))).(\lambda (H9: (eq T (THead (Flat Cast) v2 t5) t0)).(eq_ind C c0 
+(\lambda (c2: C).((eq T (THead (Flat Cast) v1 t4) (THead (Bind b) u0 t2)) \to 
+((eq T (THead (Flat Cast) v2 t5) t0) \to ((tau0 g c2 v1 v2) \to ((tau0 g c2 
+t4 t5) \to (ty3 g c0 (THead (Bind b) u0 t2) t0)))))) (\lambda (H10: (eq T 
+(THead (Flat Cast) v1 t4) (THead (Bind b) u0 t2))).(let H11 \def (eq_ind T 
+(THead (Flat Cast) v1 t4) (\lambda (e: T).(match e in T return (\lambda (_: 
 T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | 
 (THead k _ _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
 [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind 
-b) u0 t2) H11) in (False_ind ((eq T (THead (Flat Appl) v t6) t4) \to ((tau0 g 
-c0 t5 t6) \to (ty3 g c0 (THead (Bind b) u0 t2) t4))) H12))) c1 (sym_eq C c1 
-c0 H8) H9 H10 H7)))) | (tau0_cast c1 v1 v2 H7 t5 t6 H8) \Rightarrow (\lambda 
-(H9: (eq C c1 c0)).(\lambda (H10: (eq T (THead (Flat Cast) v1 t5) (THead 
-(Bind b) u0 t2))).(\lambda (H11: (eq T (THead (Flat Cast) v2 t6) t4)).(eq_ind 
-C c0 (\lambda (c2: C).((eq T (THead (Flat Cast) v1 t5) (THead (Bind b) u0 
-t2)) \to ((eq T (THead (Flat Cast) v2 t6) t4) \to ((tau0 g c2 v1 v2) \to 
-((tau0 g c2 t5 t6) \to (ty3 g c0 (THead (Bind b) u0 t2) t4)))))) (\lambda 
-(H12: (eq T (THead (Flat Cast) v1 t5) (THead (Bind b) u0 t2))).(let H13 \def 
-(eq_ind T (THead (Flat Cast) v1 t5) (\lambda (e: T).(match e in T return 
-(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) 
-\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda 
-(_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow 
-True])])) I (THead (Bind b) u0 t2) H12) in (False_ind ((eq T (THead (Flat 
-Cast) v2 t6) t4) \to ((tau0 g c0 v1 v2) \to ((tau0 g c0 t5 t6) \to (ty3 g c0 
-(THead (Bind b) u0 t2) t4)))) H13))) c1 (sym_eq C c1 c0 H9) H10 H11 H7 
-H8))))]) in (H7 (refl_equal C c0) (refl_equal T (THead (Bind b) u0 t2)) 
-(refl_equal T t4)))))))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda 
-(u0: T).(\lambda (H0: (ty3 g c0 w u0)).(\lambda (_: ((\forall (t2: T).((tau0 
-g c0 w t2) \to (ty3 g c0 w t2))))).(\lambda (v: T).(\lambda (t: T).(\lambda 
-(H2: (ty3 g c0 v (THead (Bind Abst) u0 t))).(\lambda (H3: ((\forall (t2: 
-T).((tau0 g c0 v t2) \to (ty3 g c0 v t2))))).(\lambda (t2: T).(\lambda (H4: 
-(tau0 g c0 (THead (Flat Appl) w v) t2)).(let H5 \def (match H4 in tau0 return 
-(\lambda (c1: C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (tau0 ? c1 t0 
-t3)).((eq C c1 c0) \to ((eq T t0 (THead (Flat Appl) w v)) \to ((eq T t3 t2) 
-\to (ty3 g c0 (THead (Flat Appl) w v) t2)))))))) with [(tau0_sort c1 n) 
-\Rightarrow (\lambda (H5: (eq C c1 c0)).(\lambda (H6: (eq T (TSort n) (THead 
-(Flat Appl) w v))).(\lambda (H7: (eq T (TSort (next g n)) t2)).(eq_ind C c0 
-(\lambda (_: C).((eq T (TSort n) (THead (Flat Appl) w v)) \to ((eq T (TSort 
-(next g n)) t2) \to (ty3 g c0 (THead (Flat Appl) w v) t2)))) (\lambda (H8: 
-(eq T (TSort n) (THead (Flat Appl) w v))).(let H9 \def (eq_ind T (TSort n) 
-(\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) 
-\Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow 
-False])) I (THead (Flat Appl) w v) H8) in (False_ind ((eq T (TSort (next g 
-n)) t2) \to (ty3 g c0 (THead (Flat Appl) w v) t2)) H9))) c1 (sym_eq C c1 c0 
-H5) H6 H7)))) | (tau0_abbr c1 d v0 i H5 w0 H6) \Rightarrow (\lambda (H7: (eq 
-C c1 c0)).(\lambda (H8: (eq T (TLRef i) (THead (Flat Appl) w v))).(\lambda 
-(H9: (eq T (lift (S i) O w0) t2)).(eq_ind C c0 (\lambda (c2: C).((eq T (TLRef 
-i) (THead (Flat Appl) w v)) \to ((eq T (lift (S i) O w0) t2) \to ((getl i c2 
+b) u0 t2) H10) in (False_ind ((eq T (THead (Flat Cast) v2 t5) t0) \to ((tau0 
+g c0 v1 v2) \to ((tau0 g c0 t4 t5) \to (ty3 g c0 (THead (Bind b) u0 t2) 
+t0)))) H11))) c1 (sym_eq C c1 c0 H7) H8 H9 H5 H6))))]) in (H5 (refl_equal C 
+c0) (refl_equal T (THead (Bind b) u0 t2)) (refl_equal T t0))))))))))))))) 
+(\lambda (c0: C).(\lambda (w: T).(\lambda (u0: T).(\lambda (H0: (ty3 g c0 w 
+u0)).(\lambda (_: ((\forall (t2: T).((tau0 g c0 w t2) \to (ty3 g c0 w 
+t2))))).(\lambda (v: T).(\lambda (t: T).(\lambda (H2: (ty3 g c0 v (THead 
+(Bind Abst) u0 t))).(\lambda (H3: ((\forall (t2: T).((tau0 g c0 v t2) \to 
+(ty3 g c0 v t2))))).(\lambda (t2: T).(\lambda (H4: (tau0 g c0 (THead (Flat 
+Appl) w v) t2)).(let H5 \def (match H4 in tau0 return (\lambda (c1: 
+C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (tau0 ? c1 t0 t3)).((eq C 
+c1 c0) \to ((eq T t0 (THead (Flat Appl) w v)) \to ((eq T t3 t2) \to (ty3 g c0 
+(THead (Flat Appl) w v) t2)))))))) with [(tau0_sort c1 n) \Rightarrow 
+(\lambda (H5: (eq C c1 c0)).(\lambda (H6: (eq T (TSort n) (THead (Flat Appl) 
+w v))).(\lambda (H7: (eq T (TSort (next g n)) t2)).(eq_ind C c0 (\lambda (_: 
+C).((eq T (TSort n) (THead (Flat Appl) w v)) \to ((eq T (TSort (next g n)) 
+t2) \to (ty3 g c0 (THead (Flat Appl) w v) t2)))) (\lambda (H8: (eq T (TSort 
+n) (THead (Flat Appl) w v))).(let H9 \def (eq_ind T (TSort n) (\lambda (e: 
+T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow 
+True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I 
+(THead (Flat Appl) w v) H8) in (False_ind ((eq T (TSort (next g n)) t2) \to 
+(ty3 g c0 (THead (Flat Appl) w v) t2)) H9))) c1 (sym_eq C c1 c0 H5) H6 H7)))) 
+| (tau0_abbr c1 d v0 i H5 w0 H6) \Rightarrow (\lambda (H7: (eq C c1 
+c0)).(\lambda (H8: (eq T (TLRef i) (THead (Flat Appl) w v))).(\lambda (H9: 
+(eq T (lift (S i) O w0) t2)).(eq_ind C c0 (\lambda (c2: C).((eq T (TLRef i) 
+(THead (Flat Appl) w v)) \to ((eq T (lift (S i) O w0) t2) \to ((getl i c2 
 (CHead d (Bind Abbr) v0)) \to ((tau0 g d v0 w0) \to (ty3 g c0 (THead (Flat 
 Appl) w v) t2)))))) (\lambda (H10: (eq T (TLRef i) (THead (Flat Appl) w 
 v))).(let H11 \def (eq_ind T (TLRef i) (\lambda (e: T).(match e in T return 
@@ -492,26 +484,23 @@ x)).(ex_ind T (\lambda (t4: T).(ty3 g c0 u0 t4)) (ty3 g c0 (THead (Flat Appl)
 w v) (THead (Flat Appl) w t3)) (\lambda (x0: T).(\lambda (_: (ty3 g c0 u0 
 x0)).(ex_ind T (\lambda (t4: T).(ty3 g c0 (THead (Bind Abst) u0 t) t4)) (ty3 
 g c0 (THead (Flat Appl) w v) (THead (Flat Appl) w t3)) (\lambda (x1: 
-T).(\lambda (H18: (ty3 g c0 (THead (Bind Abst) u0 t) x1)).(ex4_3_ind T T T 
-(\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(pc3 c0 (THead (Bind Abst) 
-u0 t4) x1)))) (\lambda (_: T).(\lambda (t5: T).(\lambda (_: T).(ty3 g c0 u0 
-t5)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead c0 
-(Bind Abst) u0) t t4)))) (\lambda (t4: T).(\lambda (_: T).(\lambda (t6: 
-T).(ty3 g (CHead c0 (Bind Abst) u0) t4 t6)))) (ty3 g c0 (THead (Flat Appl) w 
-v) (THead (Flat Appl) w t3)) (\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: 
-T).(\lambda (_: (pc3 c0 (THead (Bind Abst) u0 x2) x1)).(\lambda (H20: (ty3 g 
-c0 u0 x3)).(\lambda (H21: (ty3 g (CHead c0 (Bind Abst) u0) t x2)).(\lambda 
-(H22: (ty3 g (CHead c0 (Bind Abst) u0) x2 x4)).(ty3_conv g c0 (THead (Flat 
-Appl) w t3) (THead (Flat Appl) w (THead (Bind Abst) u0 x2)) (ty3_appl g c0 w 
-u0 H0 t3 x2 (ty3_sconv g c0 t3 x H16 (THead (Bind Abst) u0 t) (THead (Bind 
-Abst) u0 x2) (ty3_bind g c0 u0 x3 H20 Abst t x2 H21 x4 H22) H15)) (THead 
-(Flat Appl) w v) (THead (Flat Appl) w (THead (Bind Abst) u0 t)) (ty3_appl g 
-c0 w u0 H0 v t H2) (pc3_s c0 (THead (Flat Appl) w (THead (Bind Abst) u0 t)) 
-(THead (Flat Appl) w t3) (pc3_thin_dx c0 t3 (THead (Bind Abst) u0 t) H15 w 
-Appl)))))))))) (ty3_gen_bind g Abst c0 u0 t x1 H18)))) (ty3_correct g c0 v 
-(THead (Bind Abst) u0 t) H2)))) (ty3_correct g c0 w u0 H0)))) (ty3_correct g 
-c0 v t3 H_y))))) t2 H13)) t0 (sym_eq T t0 v H12))) v0 (sym_eq T v0 w H11))) 
-H10))) c1 (sym_eq C c1 c0 H6) H7 H8 H5)))) | (tau0_cast c1 v1 v2 H5 t0 t3 H6) 
+T).(\lambda (H18: (ty3 g c0 (THead (Bind Abst) u0 t) x1)).(ex3_2_ind T T 
+(\lambda (t4: T).(\lambda (_: T).(pc3 c0 (THead (Bind Abst) u0 t4) x1))) 
+(\lambda (_: T).(\lambda (t5: T).(ty3 g c0 u0 t5))) (\lambda (t4: T).(\lambda 
+(_: T).(ty3 g (CHead c0 (Bind Abst) u0) t t4))) (ty3 g c0 (THead (Flat Appl) 
+w v) (THead (Flat Appl) w t3)) (\lambda (x2: T).(\lambda (x3: T).(\lambda (_: 
+(pc3 c0 (THead (Bind Abst) u0 x2) x1)).(\lambda (H20: (ty3 g c0 u0 
+x3)).(\lambda (H21: (ty3 g (CHead c0 (Bind Abst) u0) t x2)).(ty3_conv g c0 
+(THead (Flat Appl) w t3) (THead (Flat Appl) w (THead (Bind Abst) u0 x2)) 
+(ty3_appl g c0 w u0 H0 t3 x2 (ty3_sconv g c0 t3 x H16 (THead (Bind Abst) u0 
+t) (THead (Bind Abst) u0 x2) (ty3_bind g c0 u0 x3 H20 Abst t x2 H21) H15)) 
+(THead (Flat Appl) w v) (THead (Flat Appl) w (THead (Bind Abst) u0 t)) 
+(ty3_appl g c0 w u0 H0 v t H2) (pc3_thin_dx c0 (THead (Bind Abst) u0 t) t3 
+(ty3_unique g c0 v (THead (Bind Abst) u0 t) H2 t3 H_y) w Appl))))))) 
+(ty3_gen_bind g Abst c0 u0 t x1 H18)))) (ty3_correct g c0 v (THead (Bind 
+Abst) u0 t) H2)))) (ty3_correct g c0 w u0 H0)))) (ty3_correct g c0 v t3 
+H_y))))) t2 H13)) t0 (sym_eq T t0 v H12))) v0 (sym_eq T v0 w H11))) H10))) c1 
+(sym_eq C c1 c0 H6) H7 H8 H5)))) | (tau0_cast c1 v1 v2 H5 t0 t3 H6) 
 \Rightarrow (\lambda (H7: (eq C c1 c0)).(\lambda (H8: (eq T (THead (Flat 
 Cast) v1 t0) (THead (Flat Appl) w v))).(\lambda (H9: (eq T (THead (Flat Cast) 
 v2 t3) t2)).(eq_ind C c0 (\lambda (c2: C).((eq T (THead (Flat Cast) v1 t0) 
@@ -625,10 +614,9 @@ t3 t2) (THead (Flat Cast) v2 t6)) (\lambda (x0: T).(\lambda (H19: (ty3 g c0
 t6 x0)).(ty3_conv g c0 (THead (Flat Cast) v2 t6) (THead (Flat Cast) x v2) 
 (ty3_cast g c0 t6 v2 (ty3_sconv g c0 t6 x0 H19 t3 v2 H_y0 H17) x H18) (THead 
 (Flat Cast) t3 t2) (THead (Flat Cast) v2 t3) (ty3_cast g c0 t2 t3 H0 v2 H_y0) 
-(pc3_s c0 (THead (Flat Cast) v2 t3) (THead (Flat Cast) v2 t6) (pc3_thin_dx c0 
-t6 t3 H17 v2 Cast))))) (ty3_correct g c0 t2 t6 H_y)))) (ty3_correct g c0 t3 
-v2 H_y0))))))) t4 H14)) t5 (sym_eq T t5 t2 H13))) v1 (sym_eq T v1 t3 H12))) 
-H11))) c1 (sym_eq C c1 c0 H7) H8 H9 H5 H6))))]) in (H5 (refl_equal C c0) 
-(refl_equal T (THead (Flat Cast) t3 t2)) (refl_equal T t4))))))))))))) c u t1 
-H))))).
+(pc3_thin_dx c0 t3 t6 (ty3_unique g c0 t2 t3 H0 t6 H_y) v2 Cast)))) 
+(ty3_correct g c0 t2 t6 H_y)))) (ty3_correct g c0 t3 v2 H_y0))))))) t4 H14)) 
+t5 (sym_eq T t5 t2 H13))) v1 (sym_eq T v1 t3 H12))) H11))) c1 (sym_eq C c1 c0 
+H7) H8 H9 H5 H6))))]) in (H5 (refl_equal C c0) (refl_equal T (THead (Flat 
+Cast) t3 t2)) (refl_equal T t4))))))))))))) c u t1 H))))).