X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fpr3%2Fwcpr0.ma;h=1469dbf9fb2dbed3ea6d894f6a78fd864a65c973;hb=99f153e43f18bc682339bed41c8230af2ac6fd2f;hp=0d8c422ba5a904bf8668bd0b4cf59a3f548598a1;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma
index 0d8c422ba..1469dbf9f 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+include "LambdaDelta-1/pr3/props.ma".
 
-
-include "pr3/props.ma".
-
-include "wcpr0/getl.ma".
+include "LambdaDelta-1/wcpr0/getl.ma".
 
 theorem pr3_wcpr0_t:
  \forall (c1: C).(\forall (c2: C).((wcpr0 c2 c1) \to (\forall (t1: 
@@ -36,44 +34,30 @@ T).(\lambda (H3: (pr3 (CHead c3 k u2) t1 t2)).(pr3_ind (CHead c3 k u1)
 T).(pr3_refl (CHead c0 k u1) t)) (\lambda (t0: T).(\lambda (t3: T).(\lambda 
 (H4: (pr2 (CHead c3 k u1) t3 t0)).(\lambda (t4: T).(\lambda (_: (pr3 (CHead 
 c3 k u1) t0 t4)).(\lambda (H6: (pr3 (CHead c0 k u1) t0 t4)).(pr3_t t0 t3 
-(CHead c0 k u1) (let H7 \def (match H4 in pr2 return (\lambda (c: C).(\lambda 
-(t: T).(\lambda (t5: T).(\lambda (_: (pr2 c t t5)).((eq C c (CHead c3 k u1)) 
-\to ((eq T t t3) \to ((eq T t5 t0) \to (pr3 (CHead c0 k u1) t3 t0)))))))) 
-with [(pr2_free c t5 t6 H7) \Rightarrow (\lambda (H8: (eq C c (CHead c3 k 
-u1))).(\lambda (H9: (eq T t5 t3)).(\lambda (H10: (eq T t6 t0)).(eq_ind C 
-(CHead c3 k u1) (\lambda (_: C).((eq T t5 t3) \to ((eq T t6 t0) \to ((pr0 t5 
-t6) \to (pr3 (CHead c0 k u1) t3 t0))))) (\lambda (H11: (eq T t5 t3)).(eq_ind 
-T t3 (\lambda (t: T).((eq T t6 t0) \to ((pr0 t t6) \to (pr3 (CHead c0 k u1) 
-t3 t0)))) (\lambda (H12: (eq T t6 t0)).(eq_ind T t0 (\lambda (t: T).((pr0 t3 
-t) \to (pr3 (CHead c0 k u1) t3 t0))) (\lambda (H13: (pr0 t3 t0)).(pr3_pr2 
-(CHead c0 k u1) t3 t0 (pr2_free (CHead c0 k u1) t3 t0 H13))) t6 (sym_eq T t6 
-t0 H12))) t5 (sym_eq T t5 t3 H11))) c (sym_eq C c (CHead c3 k u1) H8) H9 H10 
-H7)))) | (pr2_delta c d u i H7 t5 t6 H8 t H9) \Rightarrow (\lambda (H10: (eq 
-C c (CHead c3 k u1))).(\lambda (H11: (eq T t5 t3)).(\lambda (H12: (eq T t 
-t0)).(eq_ind C (CHead c3 k u1) (\lambda (c4: C).((eq T t5 t3) \to ((eq T t 
-t0) \to ((getl i c4 (CHead d (Bind Abbr) u)) \to ((pr0 t5 t6) \to ((subst0 i 
-u t6 t) \to (pr3 (CHead c0 k u1) t3 t0))))))) (\lambda (H13: (eq T t5 
-t3)).(eq_ind T t3 (\lambda (t7: T).((eq T t t0) \to ((getl i (CHead c3 k u1) 
-(CHead d (Bind Abbr) u)) \to ((pr0 t7 t6) \to ((subst0 i u t6 t) \to (pr3 
-(CHead c0 k u1) t3 t0)))))) (\lambda (H14: (eq T t t0)).(eq_ind T t0 (\lambda 
-(t7: T).((getl i (CHead c3 k u1) (CHead d (Bind Abbr) u)) \to ((pr0 t3 t6) 
-\to ((subst0 i u t6 t7) \to (pr3 (CHead c0 k u1) t3 t0))))) (\lambda (H15: 
-(getl i (CHead c3 k u1) (CHead d (Bind Abbr) u))).(\lambda (H16: (pr0 t3 
-t6)).(\lambda (H17: (subst0 i u t6 t0)).(ex3_2_ind C T (\lambda (e2: 
+(CHead c0 k u1) (insert_eq C (CHead c3 k u1) (\lambda (c: C).(pr2 c t3 t0)) 
+(\lambda (_: C).(pr3 (CHead c0 k u1) t3 t0)) (\lambda (y: C).(\lambda (H7: 
+(pr2 y t3 t0)).(pr2_ind (\lambda (c: C).(\lambda (t: T).(\lambda (t5: T).((eq 
+C c (CHead c3 k u1)) \to (pr3 (CHead c0 k u1) t t5))))) (\lambda (c: 
+C).(\lambda (t5: T).(\lambda (t6: T).(\lambda (H8: (pr0 t5 t6)).(\lambda (_: 
+(eq C c (CHead c3 k u1))).(pr3_pr2 (CHead c0 k u1) t5 t6 (pr2_free (CHead c0 
+k u1) t5 t6 H8))))))) (\lambda (c: C).(\lambda (d: C).(\lambda (u: 
+T).(\lambda (i: nat).(\lambda (H8: (getl i c (CHead d (Bind Abbr) 
+u))).(\lambda (t5: T).(\lambda (t6: T).(\lambda (H9: (pr0 t5 t6)).(\lambda 
+(t: T).(\lambda (H10: (subst0 i u t6 t)).(\lambda (H11: (eq C c (CHead c3 k 
+u1))).(let H12 \def (eq_ind C c (\lambda (c4: C).(getl i c4 (CHead d (Bind 
+Abbr) u))) H8 (CHead c3 k u1) H11) in (ex3_2_ind C T (\lambda (e2: 
 C).(\lambda (u3: T).(getl i (CHead c0 k u1) (CHead e2 (Bind Abbr) u3)))) 
 (\lambda (e2: C).(\lambda (_: T).(wcpr0 e2 d))) (\lambda (_: C).(\lambda (u3: 
-T).(pr0 u3 u))) (pr3 (CHead c0 k u1) t3 t0) (\lambda (x0: C).(\lambda (x1: 
-T).(\lambda (H18: (getl i (CHead c0 k u1) (CHead x0 (Bind Abbr) 
-x1))).(\lambda (_: (wcpr0 x0 d)).(\lambda (H20: (pr0 x1 u)).(ex2_ind T 
-(\lambda (t7: T).(subst0 i x1 t6 t7)) (\lambda (t7: T).(pr0 t7 t0)) (pr3 
-(CHead c0 k u1) t3 t0) (\lambda (x: T).(\lambda (H21: (subst0 i x1 t6 
-x)).(\lambda (H22: (pr0 x t0)).(pr3_sing (CHead c0 k u1) x t3 (pr2_delta 
-(CHead c0 k u1) x0 x1 i H18 t3 t6 H16 x H21) t0 (pr3_pr2 (CHead c0 k u1) x t0 
-(pr2_free (CHead c0 k u1) x t0 H22)))))) (pr0_subst0_back u t6 t0 i H17 x1 
-H20))))))) (wcpr0_getl_back (CHead c3 k u1) (CHead c0 k u1) (wcpr0_comp c0 c3 
-H0 u1 u1 (pr0_refl u1) k) i d u (Bind Abbr) H15))))) t (sym_eq T t t0 H14))) 
-t5 (sym_eq T t5 t3 H13))) c (sym_eq C c (CHead c3 k u1) H10) H11 H12 H7 H8 
-H9))))]) in (H7 (refl_equal C (CHead c3 k u1)) (refl_equal T t3) (refl_equal 
-T t0))) t4 H6))))))) t1 t2 (pr3_pr2_pr3_t c3 u2 t1 t2 k H3 u1 (pr2_free c3 u1 
-u2 H2)))))))))))))) c2 c1 H))).
+T).(pr0 u3 u))) (pr3 (CHead c0 k u1) t5 t) (\lambda (x0: C).(\lambda (x1: 
+T).(\lambda (H13: (getl i (CHead c0 k u1) (CHead x0 (Bind Abbr) 
+x1))).(\lambda (_: (wcpr0 x0 d)).(\lambda (H15: (pr0 x1 u)).(ex2_ind T 
+(\lambda (t7: T).(subst0 i x1 t6 t7)) (\lambda (t7: T).(pr0 t7 t)) (pr3 
+(CHead c0 k u1) t5 t) (\lambda (x: T).(\lambda (H16: (subst0 i x1 t6 
+x)).(\lambda (H17: (pr0 x t)).(pr3_sing (CHead c0 k u1) x t5 (pr2_delta 
+(CHead c0 k u1) x0 x1 i H13 t5 t6 H9 x H16) t (pr3_pr2 (CHead c0 k u1) x t 
+(pr2_free (CHead c0 k u1) x t H17)))))) (pr0_subst0_back u t6 t i H10 x1 
+H15))))))) (wcpr0_getl_back (CHead c3 k u1) (CHead c0 k u1) (wcpr0_comp c0 c3 
+H0 u1 u1 (pr0_refl u1) k) i d u (Bind Abbr) H12)))))))))))))) y t3 t0 H7))) 
+H4) t4 H6))))))) t1 t2 (pr3_pr2_pr3_t c3 u2 t1 t2 k H3 u1 (pr2_free c3 u1 u2 
+H2)))))))))))))) c2 c1 H))).