X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fpr2%2Fsubst1.ma;h=936e655f152afe3fe4e7e21a67d55a59beb15f17;hb=e92710b1d9774a6491122668c8463b8658114610;hp=9d230c6b156d667b74df5c6ddd188dc531384c23;hpb=bd5488c8eaa88e27d6e9e6c46566f1ed8f1a59b0;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma
index 9d230c6b1..936e655f1 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma
@@ -14,19 +14,19 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "pr2/defs.ma".
+include "LambdaDelta-1/pr2/defs.ma".
 
-include "pr0/subst1.ma".
+include "LambdaDelta-1/pr0/subst1.ma".
 
-include "pr0/fwd.ma".
+include "LambdaDelta-1/pr0/fwd.ma".
 
-include "csubst1/getl.ma".
+include "LambdaDelta-1/csubst1/getl.ma".
 
-include "csubst1/fwd.ma".
+include "LambdaDelta-1/csubst1/fwd.ma".
 
-include "subst1/subst1.ma".
+include "LambdaDelta-1/subst1/subst1.ma".
 
-include "getl/drop.ma".
+include "LambdaDelta-1/getl/drop.ma".
 
 theorem pr2_delta1:
  \forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c 
@@ -48,80 +48,64 @@ w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2))))))))))))
 \def
  \lambda (c: C).(\lambda (e: C).(\lambda (v: T).(\lambda (i: nat).(\lambda 
 (H: (getl i c (CHead e (Bind Abbr) v))).(\lambda (t1: T).(\lambda (t2: 
-T).(\lambda (H0: (pr2 c t1 t2)).(let H1 \def (match H0 in pr2 return (\lambda 
-(c0: C).(\lambda (t: T).(\lambda (t0: T).(\lambda (_: (pr2 c0 t t0)).((eq C 
-c0 c) \to ((eq T t t1) \to ((eq T t0 t2) \to (\forall (w1: T).((subst1 i v t1 
-w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v 
-t2 w2)))))))))))) with [(pr2_free c0 t0 t3 H1) \Rightarrow (\lambda (H2: (eq 
-C c0 c)).(\lambda (H3: (eq T t0 t1)).(\lambda (H4: (eq T t3 t2)).(eq_ind C c 
-(\lambda (_: C).((eq T t0 t1) \to ((eq T t3 t2) \to ((pr0 t0 t3) \to (\forall 
-(w1: T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) 
-(\lambda (w2: T).(subst1 i v t2 w2))))))))) (\lambda (H5: (eq T t0 
-t1)).(eq_ind T t1 (\lambda (t: T).((eq T t3 t2) \to ((pr0 t t3) \to (\forall 
-(w1: T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) 
-(\lambda (w2: T).(subst1 i v t2 w2)))))))) (\lambda (H6: (eq T t3 
-t2)).(eq_ind T t2 (\lambda (t: T).((pr0 t1 t) \to (\forall (w1: T).((subst1 i 
-v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 
-i v t2 w2))))))) (\lambda (H7: (pr0 t1 t2)).(\lambda (w1: T).(\lambda (H8: 
-(subst1 i v t1 w1)).(ex2_ind T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: 
-T).(subst1 i v t2 w2)) (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: 
-T).(subst1 i v t2 w2))) (\lambda (x: T).(\lambda (H9: (pr0 w1 x)).(\lambda 
-(H10: (subst1 i v t2 x)).(ex_intro2 T (\lambda (w2: T).(pr2 c w1 w2)) 
-(\lambda (w2: T).(subst1 i v t2 w2)) x (pr2_free c w1 x H9) H10)))) 
-(pr0_subst1 t1 t2 H7 v w1 i H8 v (pr0_refl v)))))) t3 (sym_eq T t3 t2 H6))) 
-t0 (sym_eq T t0 t1 H5))) c0 (sym_eq C c0 c H2) H3 H4 H1)))) | (pr2_delta c0 d 
-u i0 H1 t0 t3 H2 t H3) \Rightarrow (\lambda (H4: (eq C c0 c)).(\lambda (H5: 
-(eq T t0 t1)).(\lambda (H6: (eq T t t2)).(eq_ind C c (\lambda (c1: C).((eq T 
-t0 t1) \to ((eq T t t2) \to ((getl i0 c1 (CHead d (Bind Abbr) u)) \to ((pr0 
-t0 t3) \to ((subst0 i0 u t3 t) \to (\forall (w1: T).((subst1 i v t1 w1) \to 
-(ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 
-w2))))))))))) (\lambda (H7: (eq T t0 t1)).(eq_ind T t1 (\lambda (t4: T).((eq 
-T t t2) \to ((getl i0 c (CHead d (Bind Abbr) u)) \to ((pr0 t4 t3) \to 
-((subst0 i0 u t3 t) \to (\forall (w1: T).((subst1 i v t1 w1) \to (ex2 T 
-(\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2)))))))))) 
-(\lambda (H8: (eq T t t2)).(eq_ind T t2 (\lambda (t4: T).((getl i0 c (CHead d 
-(Bind Abbr) u)) \to ((pr0 t1 t3) \to ((subst0 i0 u t3 t4) \to (\forall (w1: 
-T).((subst1 i v t1 w1) \to (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda 
-(w2: T).(subst1 i v t2 w2))))))))) (\lambda (H9: (getl i0 c (CHead d (Bind 
-Abbr) u))).(\lambda (H10: (pr0 t1 t3)).(\lambda (H11: (subst0 i0 u t3 
-t2)).(\lambda (w1: T).(\lambda (H12: (subst1 i v t1 w1)).(ex2_ind T (\lambda 
-(w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst1 i v t3 w2)) (ex2 T (\lambda 
-(w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2))) (\lambda (x: 
-T).(\lambda (H13: (pr0 w1 x)).(\lambda (H14: (subst1 i v t3 x)).(neq_eq_e i 
-i0 (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 
-w2))) (\lambda (H15: (not (eq nat i i0))).(ex2_ind T (\lambda (t4: T).(subst1 
-i v t2 t4)) (\lambda (t4: T).(subst1 i0 u x t4)) (ex2 T (\lambda (w2: T).(pr2 
-c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2))) (\lambda (x0: T).(\lambda 
-(H16: (subst1 i v t2 x0)).(\lambda (H17: (subst1 i0 u x x0)).(ex_intro2 T 
-(\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2)) x0 
-(pr2_delta1 c d u i0 H9 w1 x H13 x0 H17) H16)))) (subst1_confluence_neq t3 t2 
-u i0 (subst1_single i0 u t3 t2 H11) x v i H14 (sym_not_eq nat i i0 H15)))) 
-(\lambda (H15: (eq nat i i0)).(let H16 \def (eq_ind_r nat i0 (\lambda (n: 
-nat).(subst0 n u t3 t2)) H11 i H15) in (let H17 \def (eq_ind_r nat i0 
-(\lambda (n: nat).(getl n c (CHead d (Bind Abbr) u))) H9 i H15) in (let H18 
-\def (eq_ind C (CHead e (Bind Abbr) v) (\lambda (c1: C).(getl i c c1)) H 
+T).(\lambda (H0: (pr2 c t1 t2)).(insert_eq C c (\lambda (c0: C).(pr2 c0 t1 
+t2)) (\lambda (c0: C).(\forall (w1: T).((subst1 i v t1 w1) \to (ex2 T 
+(\lambda (w2: T).(pr2 c0 w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2)))))) 
+(\lambda (y: C).(\lambda (H1: (pr2 y t1 t2)).(pr2_ind (\lambda (c0: 
+C).(\lambda (t: T).(\lambda (t0: T).((eq C c0 c) \to (\forall (w1: 
+T).((subst1 i v t w1) \to (ex2 T (\lambda (w2: T).(pr2 c0 w1 w2)) (\lambda 
+(w2: T).(subst1 i v t0 w2))))))))) (\lambda (c0: C).(\lambda (t3: T).(\lambda 
+(t4: T).(\lambda (H2: (pr0 t3 t4)).(\lambda (H3: (eq C c0 c)).(\lambda (w1: 
+T).(\lambda (H4: (subst1 i v t3 w1)).(eq_ind_r C c (\lambda (c1: C).(ex2 T 
+(\lambda (w2: T).(pr2 c1 w1 w2)) (\lambda (w2: T).(subst1 i v t4 w2)))) 
+(ex2_ind T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst1 i v t4 w2)) 
+(ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t4 w2))) 
+(\lambda (x: T).(\lambda (H5: (pr0 w1 x)).(\lambda (H6: (subst1 i v t4 
+x)).(ex_intro2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v 
+t4 w2)) x (pr2_free c w1 x H5) H6)))) (pr0_subst1 t3 t4 H2 v w1 i H4 v 
+(pr0_refl v))) c0 H3)))))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u: 
+T).(\lambda (i0: nat).(\lambda (H2: (getl i0 c0 (CHead d (Bind Abbr) 
+u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H3: (pr0 t3 t4)).(\lambda 
+(t: T).(\lambda (H4: (subst0 i0 u t4 t)).(\lambda (H5: (eq C c0 c)).(\lambda 
+(w1: T).(\lambda (H6: (subst1 i v t3 w1)).(let H7 \def (eq_ind C c0 (\lambda 
+(c1: C).(getl i0 c1 (CHead d (Bind Abbr) u))) H2 c H5) in (eq_ind_r C c 
+(\lambda (c1: C).(ex2 T (\lambda (w2: T).(pr2 c1 w1 w2)) (\lambda (w2: 
+T).(subst1 i v t w2)))) (ex2_ind T (\lambda (w2: T).(pr0 w1 w2)) (\lambda 
+(w2: T).(subst1 i v t4 w2)) (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda 
+(w2: T).(subst1 i v t w2))) (\lambda (x: T).(\lambda (H8: (pr0 w1 
+x)).(\lambda (H9: (subst1 i v t4 x)).(neq_eq_e i i0 (ex2 T (\lambda (w2: 
+T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t w2))) (\lambda (H10: (not 
+(eq nat i i0))).(ex2_ind T (\lambda (t0: T).(subst1 i v t t0)) (\lambda (t0: 
+T).(subst1 i0 u x t0)) (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: 
+T).(subst1 i v t w2))) (\lambda (x0: T).(\lambda (H11: (subst1 i v t 
+x0)).(\lambda (H12: (subst1 i0 u x x0)).(ex_intro2 T (\lambda (w2: T).(pr2 c 
+w1 w2)) (\lambda (w2: T).(subst1 i v t w2)) x0 (pr2_delta1 c d u i0 H7 w1 x 
+H8 x0 H12) H11)))) (subst1_confluence_neq t4 t u i0 (subst1_single i0 u t4 t 
+H4) x v i H9 (sym_not_eq nat i i0 H10)))) (\lambda (H10: (eq nat i i0)).(let 
+H11 \def (eq_ind_r nat i0 (\lambda (n: nat).(subst0 n u t4 t)) H4 i H10) in 
+(let H12 \def (eq_ind_r nat i0 (\lambda (n: nat).(getl n c (CHead d (Bind 
+Abbr) u))) H7 i H10) in (let H13 \def (eq_ind C (CHead e (Bind Abbr) v) 
+(\lambda (c1: C).(getl i c c1)) H (CHead d (Bind Abbr) u) (getl_mono c (CHead 
+e (Bind Abbr) v) i H (CHead d (Bind Abbr) u) H12)) in (let H14 \def (f_equal 
+C C (\lambda (e0: C).(match e0 in C return (\lambda (_: C).C) with [(CSort _) 
+\Rightarrow e | (CHead c1 _ _) \Rightarrow c1])) (CHead e (Bind Abbr) v) 
 (CHead d (Bind Abbr) u) (getl_mono c (CHead e (Bind Abbr) v) i H (CHead d 
-(Bind Abbr) u) H17)) in (let H19 \def (f_equal C C (\lambda (e0: C).(match e0 
-in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow e | (CHead c1 _ _) 
-\Rightarrow c1])) (CHead e (Bind Abbr) v) (CHead d (Bind Abbr) u) (getl_mono 
-c (CHead e (Bind Abbr) v) i H (CHead d (Bind Abbr) u) H17)) in ((let H20 \def 
-(f_equal C T (\lambda (e0: C).(match e0 in C return (\lambda (_: C).T) with 
-[(CSort _) \Rightarrow v | (CHead _ _ t4) \Rightarrow t4])) (CHead e (Bind 
-Abbr) v) (CHead d (Bind Abbr) u) (getl_mono c (CHead e (Bind Abbr) v) i H 
-(CHead d (Bind Abbr) u) H17)) in (\lambda (H21: (eq C e d)).(let H22 \def 
-(eq_ind_r T u (\lambda (t4: T).(getl i c (CHead d (Bind Abbr) t4))) H18 v 
-H20) in (let H23 \def (eq_ind_r T u (\lambda (t4: T).(subst0 i t4 t3 t2)) H16 
-v H20) in (let H24 \def (eq_ind_r C d (\lambda (c1: C).(getl i c (CHead c1 
-(Bind Abbr) v))) H22 e H21) in (ex2_ind T (\lambda (t4: T).(subst1 i v t2 
-t4)) (\lambda (t4: T).(subst1 i v x t4)) (ex2 T (\lambda (w2: T).(pr2 c w1 
-w2)) (\lambda (w2: T).(subst1 i v t2 w2))) (\lambda (x0: T).(\lambda (H25: 
-(subst1 i v t2 x0)).(\lambda (H26: (subst1 i v x x0)).(ex_intro2 T (\lambda 
-(w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t2 w2)) x0 (pr2_delta1 c 
-e v i H24 w1 x H13 x0 H26) H25)))) (subst1_confluence_eq t3 t2 v i 
-(subst1_single i v t3 t2 H23) x H14))))))) H19)))))))))) (pr0_subst1 t1 t3 
-H10 v w1 i H12 v (pr0_refl v)))))))) t (sym_eq T t t2 H8))) t0 (sym_eq T t0 
-t1 H7))) c0 (sym_eq C c0 c H4) H5 H6 H1 H2 H3))))]) in (H1 (refl_equal C c) 
-(refl_equal T t1) (refl_equal T t2)))))))))).
+(Bind Abbr) u) H12)) in ((let H15 \def (f_equal C T (\lambda (e0: C).(match 
+e0 in C return (\lambda (_: C).T) with [(CSort _) \Rightarrow v | (CHead _ _ 
+t0) \Rightarrow t0])) (CHead e (Bind Abbr) v) (CHead d (Bind Abbr) u) 
+(getl_mono c (CHead e (Bind Abbr) v) i H (CHead d (Bind Abbr) u) H12)) in 
+(\lambda (H16: (eq C e d)).(let H17 \def (eq_ind_r T u (\lambda (t0: T).(getl 
+i c (CHead d (Bind Abbr) t0))) H13 v H15) in (let H18 \def (eq_ind_r T u 
+(\lambda (t0: T).(subst0 i t0 t4 t)) H11 v H15) in (let H19 \def (eq_ind_r C 
+d (\lambda (c1: C).(getl i c (CHead c1 (Bind Abbr) v))) H17 e H16) in 
+(ex2_ind T (\lambda (t0: T).(subst1 i v t t0)) (\lambda (t0: T).(subst1 i v x 
+t0)) (ex2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: T).(subst1 i v t 
+w2))) (\lambda (x0: T).(\lambda (H20: (subst1 i v t x0)).(\lambda (H21: 
+(subst1 i v x x0)).(ex_intro2 T (\lambda (w2: T).(pr2 c w1 w2)) (\lambda (w2: 
+T).(subst1 i v t w2)) x0 (pr2_delta1 c e v i H19 w1 x H8 x0 H21) H20)))) 
+(subst1_confluence_eq t4 t v i (subst1_single i v t4 t H18) x H9))))))) 
+H14)))))))))) (pr0_subst1 t3 t4 H3 v w1 i H6 v (pr0_refl v))) c0 
+H5))))))))))))))) y t1 t2 H1))) H0)))))))).
 
 theorem pr2_gen_cabbr:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall