X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fpr0%2Fprops.ma;h=7e0cd81903d5461ab62d4f2081a44eb4f645e15d;hb=3b2361afb73203749541ad07e94648da6057ae67;hp=a55260e650932476469e8b46c6a45de337794ca9;hpb=413007de240fefb28650bb5ba7940f46db656751;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma
index a55260e65..7e0cd8190 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma
@@ -123,9 +123,9 @@ O) O t3)) (lift_d t3 h (S O) d O (le_O_n d))) (S d) (refl_equal nat (S d)))
 (pr0 t3 t4)).(\lambda (H1: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h 
 d t3) (lift h d t4)))))).(\lambda (u: T).(\lambda (h: nat).(\lambda (d: 
 nat).(eq_ind_r T (THead (Flat Cast) (lift h d u) (lift h (s (Flat Cast) d) 
-t3)) (\lambda (t: T).(pr0 t (lift h d t4))) (pr0_epsilon (lift h (s (Flat 
-Cast) d) t3) (lift h d t4) (H1 h d) (lift h d u)) (lift h d (THead (Flat 
-Cast) u t3)) (lift_head (Flat Cast) u t3 h d))))))))) t1 t2 H))).
+t3)) (\lambda (t: T).(pr0 t (lift h d t4))) (pr0_tau (lift h (s (Flat Cast) 
+d) t3) (lift h d t4) (H1 h d) (lift h d u)) (lift h d (THead (Flat Cast) u 
+t3)) (lift_head (Flat Cast) u t3 h d))))))))) t1 t2 H))).
 
 theorem pr0_subst0_back:
  \forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst0 
@@ -1689,58 +1689,58 @@ Cast) u2 t3))) (\lambda (u2: T).(subst0 i v1 u u2)) (or (pr0 w1 t4) (ex2 T
 T).(or (pr0 t t4) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: 
 T).(subst0 i v2 t4 w2))))) (or_introl (pr0 (THead (Flat Cast) x t3) t4) (ex2 
 T (\lambda (w2: T).(pr0 (THead (Flat Cast) x t3) w2)) (\lambda (w2: 
-T).(subst0 i v2 t4 w2))) (pr0_epsilon t3 t4 H0 x)) w1 H5)))) H4)) (\lambda 
-(H4: (ex2 T (\lambda (t5: T).(eq T w1 (THead (Flat Cast) u t5))) (\lambda 
-(t5: T).(subst0 (s (Flat Cast) i) v1 t3 t5)))).(ex2_ind T (\lambda (t5: 
-T).(eq T w1 (THead (Flat Cast) u t5))) (\lambda (t5: T).(subst0 (s (Flat 
-Cast) i) v1 t3 t5)) (or (pr0 w1 t4) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) 
-(\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x: T).(\lambda (H5: (eq T 
-w1 (THead (Flat Cast) u x))).(\lambda (H6: (subst0 (s (Flat Cast) i) v1 t3 
-x)).(eq_ind_r T (THead (Flat Cast) u x) (\lambda (t: T).(or (pr0 t t4) (ex2 T 
-(\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))))) (or_ind 
-(pr0 x t4) (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s 
-(Flat Cast) i) v2 t4 w2))) (or (pr0 (THead (Flat Cast) u x) t4) (ex2 T 
+T).(subst0 i v2 t4 w2))) (pr0_tau t3 t4 H0 x)) w1 H5)))) H4)) (\lambda (H4: 
+(ex2 T (\lambda (t5: T).(eq T w1 (THead (Flat Cast) u t5))) (\lambda (t5: 
+T).(subst0 (s (Flat Cast) i) v1 t3 t5)))).(ex2_ind T (\lambda (t5: T).(eq T 
+w1 (THead (Flat Cast) u t5))) (\lambda (t5: T).(subst0 (s (Flat Cast) i) v1 
+t3 t5)) (or (pr0 w1 t4) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: 
+T).(subst0 i v2 t4 w2)))) (\lambda (x: T).(\lambda (H5: (eq T w1 (THead (Flat 
+Cast) u x))).(\lambda (H6: (subst0 (s (Flat Cast) i) v1 t3 x)).(eq_ind_r T 
+(THead (Flat Cast) u x) (\lambda (t: T).(or (pr0 t t4) (ex2 T (\lambda (w2: 
+T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))))) (or_ind (pr0 x t4) 
+(ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Flat Cast) 
+i) v2 t4 w2))) (or (pr0 (THead (Flat Cast) u x) t4) (ex2 T (\lambda (w2: 
+T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) 
+(\lambda (H7: (pr0 x t4)).(or_introl (pr0 (THead (Flat Cast) u x) t4) (ex2 T 
 (\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i 
-v2 t4 w2)))) (\lambda (H7: (pr0 x t4)).(or_introl (pr0 (THead (Flat Cast) u 
-x) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda 
-(w2: T).(subst0 i v2 t4 w2))) (pr0_epsilon x t4 H7 u))) (\lambda (H7: (ex2 T 
+v2 t4 w2))) (pr0_tau x t4 H7 u))) (\lambda (H7: (ex2 T (\lambda (w2: T).(pr0 
+x w2)) (\lambda (w2: T).(subst0 (s (Flat Cast) i) v2 t4 w2)))).(ex2_ind T 
 (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Flat Cast) i) v2 t4 
-w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s 
-(Flat Cast) i) v2 t4 w2)) (or (pr0 (THead (Flat Cast) u x) t4) (ex2 T 
-(\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i 
-v2 t4 w2)))) (\lambda (x0: T).(\lambda (H8: (pr0 x x0)).(\lambda (H9: (subst0 
-(s (Flat Cast) i) v2 t4 x0)).(or_intror (pr0 (THead (Flat Cast) u x) t4) (ex2 
-T (\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 
-i v2 t4 w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2)) 
-(\lambda (w2: T).(subst0 i v2 t4 w2)) x0 (pr0_epsilon x x0 H8 u) H9))))) H7)) 
-(H1 v1 x (s (Flat Cast) i) H6 v2 H3)) w1 H5)))) H4)) (\lambda (H4: (ex3_2 T T 
-(\lambda (u2: T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5)))) 
-(\lambda (u2: T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_: 
-T).(\lambda (t5: T).(subst0 (s (Flat Cast) i) v1 t3 t5))))).(ex3_2_ind T T 
-(\lambda (u2: T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5)))) 
-(\lambda (u2: T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_: 
-T).(\lambda (t5: T).(subst0 (s (Flat Cast) i) v1 t3 t5))) (or (pr0 w1 t4) 
-(ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) 
-(\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (eq T w1 (THead (Flat Cast) 
-x0 x1))).(\lambda (_: (subst0 i v1 u x0)).(\lambda (H7: (subst0 (s (Flat 
-Cast) i) v1 t3 x1)).(eq_ind_r T (THead (Flat Cast) x0 x1) (\lambda (t: T).(or 
-(pr0 t t4) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2 
-t4 w2))))) (or_ind (pr0 x1 t4) (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda 
+w2)) (or (pr0 (THead (Flat Cast) u x) t4) (ex2 T (\lambda (w2: T).(pr0 (THead 
+(Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x0: 
+T).(\lambda (H8: (pr0 x x0)).(\lambda (H9: (subst0 (s (Flat Cast) i) v2 t4 
+x0)).(or_intror (pr0 (THead (Flat Cast) u x) t4) (ex2 T (\lambda (w2: T).(pr0 
+(THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) 
+(ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda (w2: 
+T).(subst0 i v2 t4 w2)) x0 (pr0_tau x x0 H8 u) H9))))) H7)) (H1 v1 x (s (Flat 
+Cast) i) H6 v2 H3)) w1 H5)))) H4)) (\lambda (H4: (ex3_2 T T (\lambda (u2: 
+T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5)))) (\lambda (u2: 
+T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_: T).(\lambda (t5: 
+T).(subst0 (s (Flat Cast) i) v1 t3 t5))))).(ex3_2_ind T T (\lambda (u2: 
+T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5)))) (\lambda (u2: 
+T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_: T).(\lambda (t5: 
+T).(subst0 (s (Flat Cast) i) v1 t3 t5))) (or (pr0 w1 t4) (ex2 T (\lambda (w2: 
+T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x0: 
+T).(\lambda (x1: T).(\lambda (H5: (eq T w1 (THead (Flat Cast) x0 
+x1))).(\lambda (_: (subst0 i v1 u x0)).(\lambda (H7: (subst0 (s (Flat Cast) 
+i) v1 t3 x1)).(eq_ind_r T (THead (Flat Cast) x0 x1) (\lambda (t: T).(or (pr0 
+t t4) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2 t4 
+w2))))) (or_ind (pr0 x1 t4) (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda 
 (w2: T).(subst0 (s (Flat Cast) i) v2 t4 w2))) (or (pr0 (THead (Flat Cast) x0 
 x1) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) x0 x1) w2)) (\lambda 
 (w2: T).(subst0 i v2 t4 w2)))) (\lambda (H8: (pr0 x1 t4)).(or_introl (pr0 
 (THead (Flat Cast) x0 x1) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) 
-x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (pr0_epsilon x1 t4 H8 
-x0))) (\lambda (H8: (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2: 
-T).(subst0 (s (Flat Cast) i) v2 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x1 
-w2)) (\lambda (w2: T).(subst0 (s (Flat Cast) i) v2 t4 w2)) (or (pr0 (THead 
+x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (pr0_tau x1 t4 H8 x0))) 
+(\lambda (H8: (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2: T).(subst0 
+(s (Flat Cast) i) v2 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x1 w2)) 
+(\lambda (w2: T).(subst0 (s (Flat Cast) i) v2 t4 w2)) (or (pr0 (THead (Flat 
+Cast) x0 x1) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) x0 x1) w2)) 
+(\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x: T).(\lambda (H9: (pr0 x1 
+x)).(\lambda (H10: (subst0 (s (Flat Cast) i) v2 t4 x)).(or_intror (pr0 (THead 
 (Flat Cast) x0 x1) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) x0 x1) 
-w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x: T).(\lambda (H9: 
-(pr0 x1 x)).(\lambda (H10: (subst0 (s (Flat Cast) i) v2 t4 x)).(or_intror 
-(pr0 (THead (Flat Cast) x0 x1) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat 
-Cast) x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (ex_intro2 T 
-(\lambda (w2: T).(pr0 (THead (Flat Cast) x0 x1) w2)) (\lambda (w2: T).(subst0 
-i v2 t4 w2)) x (pr0_epsilon x1 x H9 x0) H10))))) H8)) (H1 v1 x1 (s (Flat 
-Cast) i) H7 v2 H3)) w1 H5)))))) H4)) (subst0_gen_head (Flat Cast) v1 u t3 w1 
-i H2))))))))))))) t1 t2 H))).
+w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (ex_intro2 T (\lambda (w2: 
+T).(pr0 (THead (Flat Cast) x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)) 
+x (pr0_tau x1 x H9 x0) H10))))) H8)) (H1 v1 x1 (s (Flat Cast) i) H7 v2 H3)) 
+w1 H5)))))) H4)) (subst0_gen_head (Flat Cast) v1 u t3 w1 i H2))))))))))))) t1 
+t2 H))).