X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fty3%2Fpr3.ma;h=41a31b1f003b2ce59ccf4f6c961736da23068978;hb=7048db496643fc440aebc6e85dd425886bcd2e56;hp=659b8fd8492aea4a473c20252266bed7dfd95a50;hpb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma
index 659b8fd84..41a31b1f0 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma
@@ -288,12 +288,12 @@ t4 H17 (S O) O))))) (ty3_correct g (CHead c2 (Bind b) u) (lift (S O) O t4) t3
 (H18 (CHead c2 (Bind b) u) (wcpr0_comp c c2 H4 u u (pr0_refl u) (Bind b)) 
 (lift (S O) O t4) (pr0_lift t5 t4 H17 (S O) O)))))))) t6 (sym_eq T t6 t4 
 H15))) t2 H14)) u0 (sym_eq T u0 u H13))) b0 (sym_eq B b0 b H12))) H11)) H10)) 
-H9 H6 H7))) | (pr0_epsilon t5 t6 H6 u0) \Rightarrow (\lambda (H7: (eq T 
-(THead (Flat Cast) u0 t5) (THead (Bind b) u t2))).(\lambda (H8: (eq T t6 
-t4)).((let H9 \def (eq_ind T (THead (Flat Cast) u0 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 
+H9 H6 H7))) | (pr0_tau t5 t6 H6 u0) \Rightarrow (\lambda (H7: (eq T (THead 
+(Flat Cast) u0 t5) (THead (Bind b) u t2))).(\lambda (H8: (eq T t6 t4)).((let 
+H9 \def (eq_ind T (THead (Flat Cast) u0 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) u t2) H7) in (False_ind ((eq T t6 t4) \to ((pr0 
 t5 t6) \to (ty3 g c2 t4 (THead (Bind b) u t3)))) H9)) H8 H6)))]) in (H6 
 (refl_equal T (THead (Bind b) u t2)) (refl_equal T t4))))))))))))))))) 
@@ -535,7 +535,7 @@ T (THead (Bind b) u0 (lift (S O) O t3)) (\lambda (e: T).(match e in T return
 (_: K).Prop) with [(Bind _) \Rightarrow True | (Flat _) \Rightarrow 
 False])])) I (THead (Flat Appl) w v) H8) in (False_ind ((eq T t4 t2) \to 
 ((not (eq B b Abst)) \to ((pr0 t3 t4) \to (ty3 g c2 t2 (THead (Flat Appl) w 
-(THead (Bind Abst) u t0)))))) H10)) H9 H6 H7))) | (pr0_epsilon t3 t4 H6 u0) 
+(THead (Bind Abst) u t0)))))) H10)) H9 H6 H7))) | (pr0_tau t3 t4 H6 u0) 
 \Rightarrow (\lambda (H7: (eq T (THead (Flat Cast) u0 t3) (THead (Flat Appl) 
 w v))).(\lambda (H8: (eq T t4 t2)).((let H9 \def (eq_ind T (THead (Flat Cast) 
 u0 t3) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with 
@@ -635,8 +635,8 @@ T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
 [(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (THead (Flat 
 Cast) t3 t2) H8) in (False_ind ((eq T t6 t4) \to ((not (eq B b Abst)) \to 
 ((pr0 t5 t6) \to (ty3 g c2 t4 (THead (Flat Cast) t0 t3))))) H10)) H9 H6 H7))) 
-| (pr0_epsilon t5 t6 H6 u) \Rightarrow (\lambda (H7: (eq T (THead (Flat Cast) 
-u t5) (THead (Flat Cast) t3 t2))).(\lambda (H8: (eq T t6 t4)).((let H9 \def 
+| (pr0_tau t5 t6 H6 u) \Rightarrow (\lambda (H7: (eq T (THead (Flat Cast) u 
+t5) (THead (Flat Cast) t3 t2))).(\lambda (H8: (eq T t6 t4)).((let H9 \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 (Flat Cast) u t5) (THead (Flat Cast) t3 t2) H7) in 
@@ -653,10 +653,10 @@ g c2 t4 (THead (Flat Cast) t0 t3)) (\lambda (x: T).(\lambda (H14: (ty3 g c2
 t0 x)).(ty3_conv g c2 (THead (Flat Cast) t0 t3) (THead (Flat Cast) x t0) 
 (ty3_cast g c2 t3 t0 (H3 c2 H4 t3 (pr0_refl t3)) x H14) t4 t3 (H1 c2 H4 t4 
 H13) (pc3_pr2_x c2 t3 (THead (Flat Cast) t0 t3) (pr2_free c2 (THead (Flat 
-Cast) t0 t3) t3 (pr0_epsilon t3 t3 (pr0_refl t3) t0)))))) (ty3_correct g c2 
-t3 t0 (H3 c2 H4 t3 (pr0_refl t3))))) t6 (sym_eq T t6 t4 H12))) t5 (sym_eq T 
-t5 t2 H11))) u (sym_eq T u t3 H10))) H9)) H8 H6)))]) in (H6 (refl_equal T 
-(THead (Flat Cast) t3 t2)) (refl_equal T t4))))))))))))))) c1 t1 t H))))).
+Cast) t0 t3) t3 (pr0_tau t3 t3 (pr0_refl t3) t0)))))) (ty3_correct g c2 t3 t0 
+(H3 c2 H4 t3 (pr0_refl t3))))) t6 (sym_eq T t6 t4 H12))) t5 (sym_eq T t5 t2 
+H11))) u (sym_eq T u t3 H10))) H9)) H8 H6)))]) in (H6 (refl_equal T (THead 
+(Flat Cast) t3 t2)) (refl_equal T t4))))))))))))))) c1 t1 t H))))).
 
 theorem ty3_sred_pr0:
  \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (g: G).(\forall