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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma
index 9341f979b..cf432cbfc 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma
@@ -2258,22 +2258,23 @@ t3))))))))).(\lambda (u: T).(\lambda (H1: (sn3 c (THead (Flat Appl) t (THeads
 (Flat Appl) (TCons t1 t2) u)))).(\lambda (t3: T).(\lambda (H2: (sn3 c (THead 
 (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) t3)))).(let H_x \def 
 (sn3_gen_flat Appl c t (THeads (Flat Appl) (TCons t1 t2) t3) H2) in (let H3 
-\def H_x in (land_ind (sn3 c t) (sn3 c (THeads (Flat Appl) (TCons t1 t2) t3)) 
-(sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) (THead (Flat 
-Cast) u t3)))) (\lambda (_: (sn3 c t)).(\lambda (H5: (sn3 c (THeads (Flat 
-Appl) (TCons t1 t2) t3))).(let H6 \def H5 in (let H_x0 \def (sn3_gen_flat 
-Appl c t (THeads (Flat Appl) (TCons t1 t2) u) H1) in (let H7 \def H_x0 in 
-(land_ind (sn3 c t) (sn3 c (THeads (Flat Appl) (TCons t1 t2) u)) (sn3 c 
-(THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u 
-t3)))) (\lambda (H8: (sn3 c t)).(\lambda (H9: (sn3 c (THeads (Flat Appl) 
-(TCons t1 t2) u))).(let H10 \def H9 in (sn3_appl_appls t1 (THead (Flat Cast) 
-u t3) t2 c (H0 u H10 t3 H6) t H8 (\lambda (u2: T).(\lambda (H11: (pr3 c 
-(THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2)).(\lambda 
-(H12: (((iso (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2) 
-\to (\forall (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t (THeads 
-(Flat Appl) (TCons t1 t2) t3)) H2 (THead (Flat Appl) t u2) (pr3_thin_dx c 
-(THeads (Flat Appl) (TCons t1 t2) t3) u2 (pr3_iso_appls_cast c u t3 (TCons t1 
-t2) u2 H11 H12) t Appl))))))))) H7)))))) H3))))))))))) t0))) vs)).
+\def H_x in (land_ind (sn3 c t) (sn3 c (THead (Flat Appl) t1 (THeads (Flat 
+Appl) t2 t3))) (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) 
+(THead (Flat Cast) u t3)))) (\lambda (_: (sn3 c t)).(\lambda (H5: (sn3 c 
+(THead (Flat Appl) t1 (THeads (Flat Appl) t2 t3)))).(let H6 \def H5 in (let 
+H_x0 \def (sn3_gen_flat Appl c t (THeads (Flat Appl) (TCons t1 t2) u) H1) in 
+(let H7 \def H_x0 in (land_ind (sn3 c t) (sn3 c (THead (Flat Appl) t1 (THeads 
+(Flat Appl) t2 u))) (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 
+t2) (THead (Flat Cast) u t3)))) (\lambda (H8: (sn3 c t)).(\lambda (H9: (sn3 c 
+(THead (Flat Appl) t1 (THeads (Flat Appl) t2 u)))).(let H10 \def H9 in 
+(sn3_appl_appls t1 (THead (Flat Cast) u t3) t2 c (H0 u H10 t3 H6) t H8 
+(\lambda (u2: T).(\lambda (H11: (pr3 c (THeads (Flat Appl) (TCons t1 t2) 
+(THead (Flat Cast) u t3)) u2)).(\lambda (H12: (((iso (THeads (Flat Appl) 
+(TCons t1 t2) (THead (Flat Cast) u t3)) u2) \to (\forall (P: 
+Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t (THeads (Flat Appl) (TCons 
+t1 t2) t3)) H2 (THead (Flat Appl) t u2) (pr3_thin_dx c (THeads (Flat Appl) 
+(TCons t1 t2) t3) u2 (pr3_iso_appls_cast c u t3 (TCons t1 t2) u2 H11 H12) t 
+Appl))))))))) H7)))))) H3))))))))))) t0))) vs)).
 
 theorem sn3_appls_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u: 
@@ -2309,22 +2310,23 @@ T).(\lambda (H3: (sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O
 v) (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)))).(let H_x \def 
 (sn3_gen_flat Appl (CHead c (Bind b) u) (lift (S O) O v) (THeads (Flat Appl) 
 (lifts (S O) O (TCons t t0)) t1) H3) in (let H4 \def H_x in (land_ind (sn3 
-(CHead c (Bind b) u) (lift (S O) O v)) (sn3 (CHead c (Bind b) u) (THeads 
-(Flat Appl) (lifts (S O) O (TCons t t0)) t1)) (sn3 c (THead (Flat Appl) v 
-(THeads (Flat Appl) (TCons t t0) (THead (Bind b) u t1)))) (\lambda (H5: (sn3 
-(CHead c (Bind b) u) (lift (S O) O v))).(\lambda (H6: (sn3 (CHead c (Bind b) 
-u) (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1))).(let H_y \def 
-(sn3_gen_lift (CHead c (Bind b) u) v (S O) O H5 c) in (sn3_appl_appls t 
-(THead (Bind b) u t1) t0 c (H2 t1 H6) v (H_y (drop_drop (Bind b) O c c 
-(drop_refl c) u)) (\lambda (u2: T).(\lambda (H7: (pr3 c (THeads (Flat Appl) 
-(TCons t t0) (THead (Bind b) u t1)) u2)).(\lambda (H8: (((iso (THeads (Flat 
-Appl) (TCons t t0) (THead (Bind b) u t1)) u2) \to (\forall (P: 
-Prop).P)))).(let H9 \def (pr3_iso_appls_bind b H (TCons t t0) u t1 c u2 H7 
-H8) in (sn3_pr3_trans c (THead (Flat Appl) v (THead (Bind b) u (THeads (Flat 
-Appl) (lifts (S O) O (TCons t t0)) t1))) (sn3_appl_bind b H c u H0 (THeads 
-(Flat Appl) (lifts (S O) O (TCons t t0)) t1) v H3) (THead (Flat Appl) v u2) 
-(pr3_flat c v v (pr3_refl c v) (THead (Bind b) u (THeads (Flat Appl) (lifts 
-(S O) O (TCons t t0)) t1)) u2 H9 Appl)))))))))) H4))))))))) vs0))) vs)))))).
+(CHead c (Bind b) u) (lift (S O) O v)) (sn3 (CHead c (Bind b) u) (THead (Flat 
+Appl) (lift (S O) O t) (THeads (Flat Appl) (lifts (S O) O t0) t1))) (sn3 c 
+(THead (Flat Appl) v (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u 
+t1)))) (\lambda (H5: (sn3 (CHead c (Bind b) u) (lift (S O) O v))).(\lambda 
+(H6: (sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O t) (THeads 
+(Flat Appl) (lifts (S O) O t0) t1)))).(let H_y \def (sn3_gen_lift (CHead c 
+(Bind b) u) v (S O) O H5 c) in (sn3_appl_appls t (THead (Bind b) u t1) t0 c 
+(H2 t1 H6) v (H_y (drop_drop (Bind b) O c c (drop_refl c) u)) (\lambda (u2: 
+T).(\lambda (H7: (pr3 c (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u 
+t1)) u2)).(\lambda (H8: (((iso (THeads (Flat Appl) (TCons t t0) (THead (Bind 
+b) u t1)) u2) \to (\forall (P: Prop).P)))).(let H9 \def (pr3_iso_appls_bind b 
+H (TCons t t0) u t1 c u2 H7 H8) in (sn3_pr3_trans c (THead (Flat Appl) v 
+(THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1))) 
+(sn3_appl_bind b H c u H0 (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) 
+t1) v H3) (THead (Flat Appl) v u2) (pr3_flat c v v (pr3_refl c v) (THead 
+(Bind b) u (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)) u2 H9 
+Appl)))))))))) H4))))))))) vs0))) vs)))))).
 
 theorem sn3_appls_beta:
  \forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (us: TList).((sn3 c 
@@ -2361,16 +2363,16 @@ Appl) (TCons t0 t1) (THead (Bind Abbr) v t))) \to (\forall (w: T).((sn3 c w)
 (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t))))).(\lambda (w: 
 T).(\lambda (H2: (sn3 c w)).(let H_x \def (sn3_gen_flat Appl c u (THeads 
 (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)) H1) in (let H3 \def H_x in 
-(land_ind (sn3 c u) (sn3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Bind 
-Abbr) v t))) (sn3 c (THead (Flat Appl) u (THeads (Flat Appl) (TCons t0 t1) 
-(THead (Flat Appl) v (THead (Bind Abst) w t))))) (\lambda (H4: (sn3 c 
-u)).(\lambda (H5: (sn3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) 
-v t)))).(sn3_appl_appls t0 (THead (Flat Appl) v (THead (Bind Abst) w t)) t1 c 
-(H0 H5 w H2) u H4 (\lambda (u2: T).(\lambda (H6: (pr3 c (THeads (Flat Appl) 
-(TCons t0 t1) (THead (Flat Appl) v (THead (Bind Abst) w t))) u2)).(\lambda 
-(H7: (((iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Appl) v (THead 
-(Bind Abst) w t))) u2) \to (\forall (P: Prop).P)))).(let H8 \def 
-(pr3_iso_appls_beta (TCons t0 t1) v w t c u2 H6 H7) in (sn3_pr3_trans c 
+(land_ind (sn3 c u) (sn3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 
+(THead (Bind Abbr) v t)))) (sn3 c (THead (Flat Appl) u (THeads (Flat Appl) 
+(TCons t0 t1) (THead (Flat Appl) v (THead (Bind Abst) w t))))) (\lambda (H4: 
+(sn3 c u)).(\lambda (H5: (sn3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 
+(THead (Bind Abbr) v t))))).(sn3_appl_appls t0 (THead (Flat Appl) v (THead 
+(Bind Abst) w t)) t1 c (H0 H5 w H2) u H4 (\lambda (u2: T).(\lambda (H6: (pr3 
+c (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Appl) v (THead (Bind Abst) w 
+t))) u2)).(\lambda (H7: (((iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat 
+Appl) v (THead (Bind Abst) w t))) u2) \to (\forall (P: Prop).P)))).(let H8 
+\def (pr3_iso_appls_beta (TCons t0 t1) v w t c u2 H6 H7) in (sn3_pr3_trans c 
 (THead (Flat Appl) u (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v 
 t))) H1 (THead (Flat Appl) u u2) (pr3_thin_dx c (THeads (Flat Appl) (TCons t0 
 t1) (THead (Bind Abbr) v t)) u2 H8 u Appl))))))))) H3)))))))))) us0))) us)))).
@@ -2467,16 +2469,17 @@ O w))) \to (sn3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)))))).(\lambda
 (H2: (sn3 c (THead (Flat Appl) v (THeads (Flat Appl) (TCons t t0) (lift (S i) 
 O w))))).(let H_x \def (sn3_gen_flat Appl c v (THeads (Flat Appl) (TCons t 
 t0) (lift (S i) O w)) H2) in (let H3 \def H_x in (land_ind (sn3 c v) (sn3 c 
-(THeads (Flat Appl) (TCons t t0) (lift (S i) O w))) (sn3 c (THead (Flat Appl) 
-v (THeads (Flat Appl) (TCons t t0) (TLRef i)))) (\lambda (H4: (sn3 c 
-v)).(\lambda (H5: (sn3 c (THeads (Flat Appl) (TCons t t0) (lift (S i) O 
-w)))).(sn3_appl_appls t (TLRef i) t0 c (H1 H5) v H4 (\lambda (u2: T).(\lambda 
-(H6: (pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2)).(\lambda (H7: 
-(((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2) \to (\forall (P: 
-Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) v (THeads (Flat Appl) (TCons 
-t t0) (lift (S i) O w))) H2 (THead (Flat Appl) v u2) (pr3_thin_dx c (THeads 
-(Flat Appl) (TCons t t0) (lift (S i) O w)) u2 (pr3_iso_appls_abbr c d w i H 
-(TCons t t0) u2 H6 H7) v Appl)))))))) H3)))))))) vs0))) vs)))))).
+(THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w)))) (sn3 c (THead 
+(Flat Appl) v (THeads (Flat Appl) (TCons t t0) (TLRef i)))) (\lambda (H4: 
+(sn3 c v)).(\lambda (H5: (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t0 
+(lift (S i) O w))))).(sn3_appl_appls t (TLRef i) t0 c (H1 H5) v H4 (\lambda 
+(u2: T).(\lambda (H6: (pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)) 
+u2)).(\lambda (H7: (((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2) \to 
+(\forall (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) v (THeads (Flat 
+Appl) (TCons t t0) (lift (S i) O w))) H2 (THead (Flat Appl) v u2) 
+(pr3_thin_dx c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2 
+(pr3_iso_appls_abbr c d w i H (TCons t t0) u2 H6 H7) v Appl)))))))) 
+H3)))))))) vs0))) vs)))))).
 
 theorem sns3_lifts:
  \forall (c: C).(\forall (d: C).(\forall (h: nat).(\forall (i: nat).((drop h