X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Fsc3%2Fprops.ma;h=465a97ee7ba5a93c75a22cd3aebb1400bcd2b190;hb=a8fe66543d27dc771bd54eedac0b59a8718153ce;hp=23561082b268621c67c1917e8dc113fa24818f48;hpb=02bd27d53c28099b9fc92917cf34ccf3bc72d696;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma
index 23561082b..465a97ee7 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma
@@ -22,14 +22,20 @@ include "sn3/lift1.ma".
 
 include "nf2/lift1.ma".
 
+include "csuba/arity.ma".
+
 include "arity/lift1.ma".
 
 include "arity/aprem.ma".
 
 include "llt/props.ma".
 
+include "drop1/getl.ma".
+
 include "drop1/props.ma".
 
+include "lift1/props.ma".
+
 theorem sc3_arity_gen:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((sc3 g a c 
 t) \to (arity g c t a)))))
@@ -275,23 +281,25 @@ C).(\forall (w: T).((sc3 g a0 d0 w) \to (\forall (is: PList).((drop1 is d0 c)
 (THeads (Flat Appl) vs (TLRef i)))))))))) (arity_appls_abbr g c d v i H2 vs 
 (AHead a0 a1) H4) (\lambda (d0: C).(\lambda (w: T).(\lambda (H6: (sc3 g a0 d0 
 w)).(\lambda (is: PList).(\lambda (H7: (drop1 is d0 c)).(let H_x \def 
-(drop1_getl_trans is c d0 H7 Abbr d v i H2) in (let H8 \def H_x in (ex_ind C 
-(\lambda (e2: C).(getl (trans is i) d0 (CHead e2 (Bind Abbr) (ctrans is i 
-v)))) (sc3 g a1 d0 (THead (Flat Appl) w (lift1 is (THeads (Flat Appl) vs 
-(TLRef i))))) (\lambda (x: C).(\lambda (H9: (getl (trans is i) d0 (CHead x 
-(Bind Abbr) (ctrans is i v)))).(let H_y \def (H0 (TCons w (lifts1 is vs))) in 
-(eq_ind_r T (THeads (Flat Appl) (lifts1 is vs) (lift1 is (TLRef i))) (\lambda 
-(t: T).(sc3 g a1 d0 (THead (Flat Appl) w t))) (eq_ind_r T (TLRef (trans is 
-i)) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w (THeads (Flat Appl) 
-(lifts1 is vs) t)))) (H_y (trans is i) x (ctrans is i v) d0 (eq_ind T (lift1 
-is (lift (S i) O v)) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w 
-(THeads (Flat Appl) (lifts1 is vs) t)))) (eq_ind T (lift1 is (THeads (Flat 
-Appl) vs (lift (S i) O v))) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w 
-t))) (H5 d0 w H6 is H7) (THeads (Flat Appl) (lifts1 is vs) (lift1 is (lift (S 
-i) O v))) (lifts1_flat Appl is (lift (S i) O v) vs)) (lift (S (trans is i)) O 
-(ctrans is i v)) (lift1_free is i v)) H9) (lift1 is (TLRef i)) (lift1_lref is 
-i)) (lift1 is (THeads (Flat Appl) vs (TLRef i))) (lifts1_flat Appl is (TLRef 
-i) vs))))) H8))))))))))) H3))))))))))))) a)).
+(drop1_getl_trans is c d0 H7 Abbr d v i H2) in (let H8 \def H_x in (ex2_ind C 
+(\lambda (e2: C).(drop1 (ptrans is i) e2 d)) (\lambda (e2: C).(getl (trans is 
+i) d0 (CHead e2 (Bind Abbr) (lift1 (ptrans is i) v)))) (sc3 g a1 d0 (THead 
+(Flat Appl) w (lift1 is (THeads (Flat Appl) vs (TLRef i))))) (\lambda (x: 
+C).(\lambda (_: (drop1 (ptrans is i) x d)).(\lambda (H10: (getl (trans is i) 
+d0 (CHead x (Bind Abbr) (lift1 (ptrans is i) v)))).(let H_y \def (H0 (TCons w 
+(lifts1 is vs))) in (eq_ind_r T (THeads (Flat Appl) (lifts1 is vs) (lift1 is 
+(TLRef i))) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w t))) (eq_ind_r 
+T (TLRef (trans is i)) (\lambda (t: T).(sc3 g a1 d0 (THead (Flat Appl) w 
+(THeads (Flat Appl) (lifts1 is vs) t)))) (H_y (trans is i) x (lift1 (ptrans 
+is i) v) d0 (eq_ind T (lift1 is (lift (S i) O v)) (\lambda (t: T).(sc3 g a1 
+d0 (THead (Flat Appl) w (THeads (Flat Appl) (lifts1 is vs) t)))) (eq_ind T 
+(lift1 is (THeads (Flat Appl) vs (lift (S i) O v))) (\lambda (t: T).(sc3 g a1 
+d0 (THead (Flat Appl) w t))) (H5 d0 w H6 is H7) (THeads (Flat Appl) (lifts1 
+is vs) (lift1 is (lift (S i) O v))) (lifts1_flat Appl is (lift (S i) O v) 
+vs)) (lift (S (trans is i)) O (lift1 (ptrans is i) v)) (lift1_free is i v)) 
+H10) (lift1 is (TLRef i)) (lift1_lref is i)) (lift1 is (THeads (Flat Appl) vs 
+(TLRef i))) (lifts1_flat Appl is (TLRef i) vs)))))) H8))))))))))) 
+H3))))))))))))) a)).
 
 theorem sc3_cast:
  \forall (g: G).(\forall (a: A).(\forall (vs: TList).(\forall (c: C).(\forall