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=3b2361afb73203749541ad07e94648da6057ae67;hp=46d1784f60eb16dcb1f4a73662c8ca668bd87f7e;hpb=d0982534aee06a30f91a06d2f3e82834b132a3d3;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 46d1784f6..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
@@ -14,17 +14,17 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "csubt/ty3.ma".
+include "LambdaDelta-1/csubt/ty3.ma".
 
-include "ty3/subst1.ma".
+include "LambdaDelta-1/ty3/subst1.ma".
 
-include "ty3/fsubst0.ma".
+include "LambdaDelta-1/ty3/fsubst0.ma".
 
-include "pc3/pc1.ma".
+include "LambdaDelta-1/pc3/pc1.ma".
 
-include "pc3/wcpr0.ma".
+include "LambdaDelta-1/pc3/wcpr0.ma".
 
-include "pc1/props.ma".
+include "LambdaDelta-1/pc1/props.ma".
 
 theorem ty3_sred_wcpr0_pr0:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t: T).((ty3 g c1 
@@ -250,7 +250,7 @@ t3 (lift (S O) O x1))).(\lambda (H27: (ty3 g c2 x0 x1)).(let H28 \def (eq_ind
 T x0 (\lambda (t7: T).(ty3 g c2 t7 x1)) H27 t4 (lift_inj x0 t4 (S O) O 
 (subst1_gen_lift_eq t4 u (lift (S O) O x0) (S O) O O (le_n O) (eq_ind_r nat 
 (plus (S O) O) (\lambda (n: nat).(lt O n)) (le_n (plus (S O) O)) (plus O (S 
-O)) (plus_comm O (S O))) H25))) in (ty3_conv g c2 (THead (Bind Abbr) u t3) 
+O)) (plus_sym O (S O))) H25))) in (ty3_conv g c2 (THead (Bind Abbr) u t3) 
 (THead (Bind Abbr) u x) (ty3_bind g c2 u t0 (H1 c2 H4 u (pr0_refl u)) Abbr t3 
 x H22) t4 x1 H28 (pc3_pr3_x c2 x1 (THead (Bind Abbr) u t3) (pr3_t (THead 
 (Bind Abbr) u (lift (S O) O x1)) (THead (Bind Abbr) u t3) c2 (pr3_pr2 c2 
@@ -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))))))))))))))))) 
@@ -396,7 +396,7 @@ g (CHead c2 (Bind Abst) u0) t4 t5))) (ty3 g c2 (THead (Bind Abbr) v2 t4)
 (THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (x2: T).(\lambda 
 (x3: T).(\lambda (H22: (pc3 c2 (THead (Bind Abst) u0 x2) (THead (Bind Abst) u 
 t0))).(\lambda (H23: (ty3 g c2 u0 x3)).(\lambda (H24: (ty3 g (CHead c2 (Bind 
-Abst) u0) t4 x2)).(and_ind (pc3 c2 u0 u) (\forall (b: B).(\forall (u1: 
+Abst) u0) t4 x2)).(land_ind (pc3 c2 u0 u) (\forall (b: B).(\forall (u1: 
 T).(pc3 (CHead c2 (Bind b) u1) x2 t0))) (ty3 g c2 (THead (Bind Abbr) v2 t4) 
 (THead (Flat Appl) w (THead (Bind Abst) u t0))) (\lambda (H25: (pc3 c2 u0 
 u)).(\lambda (H26: ((\forall (b: B).(\forall (u1: T).(pc3 (CHead c2 (Bind b) 
@@ -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