X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fsc3%2Fprops.ma;h=b77d40402efe65977c3e65340141c4ddbedf9ff1;hb=20377cd037f6cc5eb9c6a5664354a8a0189d3f4f;hp=c1d3787b8cb2ac628abeac0e939a43c3cc5f293e;hpb=831af787465e1bff886e22ee14b68c8f1bb0177c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma
index c1d3787b8..b77d40402 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma
@@ -14,27 +14,25 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/props".
+include "LambdaDelta-1/sc3/defs.ma".
 
-include "sc3/defs.ma".
+include "LambdaDelta-1/sn3/lift1.ma".
 
-include "sn3/lift1.ma".
+include "LambdaDelta-1/nf2/lift1.ma".
 
-include "nf2/lift1.ma".
+include "LambdaDelta-1/csuba/arity.ma".
 
-include "csuba/arity.ma".
+include "LambdaDelta-1/arity/lift1.ma".
 
-include "arity/lift1.ma".
+include "LambdaDelta-1/arity/aprem.ma".
 
-include "arity/aprem.ma".
+include "LambdaDelta-1/llt/props.ma".
 
-include "llt/props.ma".
+include "LambdaDelta-1/drop1/getl.ma".
 
-include "drop1/getl.ma".
+include "LambdaDelta-1/drop1/props.ma".
 
-include "drop1/props.ma".
-
-include "lift1/props.ma".
+include "LambdaDelta-1/lift1/props.ma".
 
 theorem sc3_arity_gen:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((sc3 g a c 
@@ -74,17 +72,18 @@ c t) \to (\forall (a4: A).((leq g a3 a4) \to (sc3 g a4 c t)))))))))).(\lambda
 t))).(\lambda (a3: A).(\lambda (H1: (leq g (ASort n n0) a3)).(let H2 \def H0 
 in (and_ind (arity g c t (ASort n n0)) (sn3 c t) (sc3 g a3 c t) (\lambda (H3: 
 (arity g c t (ASort n n0))).(\lambda (H4: (sn3 c t)).(let H_y \def 
-(arity_repl g c t (ASort n n0) H3 a3 H1) in (let H_x \def (leq_gen_sort g n 
+(arity_repl g c t (ASort n n0) H3 a3 H1) in (let H_x \def (leq_gen_sort1 g n 
 n0 a3 H1) in (let H5 \def H_x in (ex2_3_ind nat nat nat (\lambda (n2: 
-nat).(\lambda (h2: nat).(\lambda (_: nat).(eq A a3 (ASort h2 n2))))) (\lambda 
-(n2: nat).(\lambda (h2: nat).(\lambda (k: nat).(eq A (aplus g (ASort n n0) k) 
-(aplus g (ASort h2 n2) k))))) (sc3 g a3 c t) (\lambda (x0: nat).(\lambda (x1: 
-nat).(\lambda (x2: nat).(\lambda (H6: (eq A a3 (ASort x1 x0))).(\lambda (_: 
-(eq A (aplus g (ASort n n0) x2) (aplus g (ASort x1 x0) x2))).(let H8 \def 
-(eq_ind A a3 (\lambda (a: A).(arity g c t a)) H_y (ASort x1 x0) H6) in 
-(eq_ind_r A (ASort x1 x0) (\lambda (a: A).(sc3 g a c t)) (conj (arity g c t 
-(ASort x1 x0)) (sn3 c t) H8 H4) a3 H6))))))) H5)))))) H2)))))))))) (\lambda 
-(a: A).(\lambda (_: ((((\forall (a3: A).((llt a3 a) \to (\forall (c: 
+nat).(\lambda (h2: nat).(\lambda (k: nat).(eq A (aplus g (ASort n n0) k) 
+(aplus g (ASort h2 n2) k))))) (\lambda (n2: nat).(\lambda (h2: nat).(\lambda 
+(_: nat).(eq A a3 (ASort h2 n2))))) (sc3 g a3 c t) (\lambda (x0: 
+nat).(\lambda (x1: nat).(\lambda (x2: nat).(\lambda (_: (eq A (aplus g (ASort 
+n n0) x2) (aplus g (ASort x1 x0) x2))).(\lambda (H7: (eq A a3 (ASort x1 
+x0))).(let H8 \def (f_equal A A (\lambda (e: A).e) a3 (ASort x1 x0) H7) in 
+(let H9 \def (eq_ind A a3 (\lambda (a: A).(arity g c t a)) H_y (ASort x1 x0) 
+H8) in (eq_ind_r A (ASort x1 x0) (\lambda (a: A).(sc3 g a c t)) (conj (arity 
+g c t (ASort x1 x0)) (sn3 c t) H9 H4) a3 H8)))))))) H5)))))) H2)))))))))) 
+(\lambda (a: A).(\lambda (_: ((((\forall (a3: A).((llt a3 a) \to (\forall (c: 
 C).(\forall (t: T).((sc3 g a3 c t) \to (\forall (a4: A).((leq g a3 a4) \to 
 (sc3 g a4 c t))))))))) \to (\forall (c: C).(\forall (t: T).((sc3 g a c t) \to 
 (\forall (a3: A).((leq g a a3) \to (sc3 g a3 c t))))))))).(\lambda (a0: 
@@ -103,24 +102,25 @@ T).((sc3 g a d w) \to (\forall (is: PList).((drop1 is d c) \to (sc3 g a0 d
 (THead (Flat Appl) w (lift1 is t)))))))) (sc3 g a3 c t) (\lambda (H5: (arity 
 g c t (AHead a a0))).(\lambda (H6: ((\forall (d: C).(\forall (w: T).((sc3 g a 
 d w) \to (\forall (is: PList).((drop1 is d c) \to (sc3 g a0 d (THead (Flat 
-Appl) w (lift1 is t)))))))))).(let H_x \def (leq_gen_head g a a0 a3 H3) in 
-(let H7 \def H_x in (ex3_2_ind A A (\lambda (a4: A).(\lambda (a5: A).(eq A a3 
-(AHead a4 a5)))) (\lambda (a4: A).(\lambda (_: A).(leq g a a4))) (\lambda (_: 
-A).(\lambda (a5: A).(leq g a0 a5))) (sc3 g a3 c t) (\lambda (x0: A).(\lambda 
-(x1: A).(\lambda (H8: (eq A a3 (AHead x0 x1))).(\lambda (H9: (leq g a 
-x0)).(\lambda (H10: (leq g a0 x1)).(eq_ind_r A (AHead x0 x1) (\lambda (a4: 
-A).(sc3 g a4 c t)) (conj (arity g c t (AHead x0 x1)) (\forall (d: C).(\forall 
-(w: T).((sc3 g x0 d w) \to (\forall (is: PList).((drop1 is d c) \to (sc3 g x1 
-d (THead (Flat Appl) w (lift1 is t)))))))) (arity_repl g c t (AHead a a0) H5 
-(AHead x0 x1) (leq_head g a x0 H9 a0 x1 H10)) (\lambda (d: C).(\lambda (w: 
-T).(\lambda (H11: (sc3 g x0 d w)).(\lambda (is: PList).(\lambda (H12: (drop1 
-is d c)).(H0 (\lambda (a4: A).(\lambda (H13: (llt a4 a0)).(\lambda (c0: 
-C).(\lambda (t0: T).(\lambda (H14: (sc3 g a4 c0 t0)).(\lambda (a5: 
-A).(\lambda (H15: (leq g a4 a5)).(H1 a4 (llt_trans a4 a0 (AHead a a0) H13 
-(llt_head_dx a a0)) c0 t0 H14 a5 H15)))))))) d (THead (Flat Appl) w (lift1 is 
-t)) (H6 d w (H1 x0 (llt_repl g a x0 H9 (AHead a a0) (llt_head_sx a a0)) d w 
-H11 a (leq_sym g a x0 H9)) is H12) x1 H10))))))) a3 H8)))))) H7))))) 
-H4)))))))))))) a2)) a1)).
+Appl) w (lift1 is t)))))))))).(let H_x \def (leq_gen_head1 g a a0 a3 H3) in 
+(let H7 \def H_x in (ex3_2_ind A A (\lambda (a4: A).(\lambda (_: A).(leq g a 
+a4))) (\lambda (_: A).(\lambda (a5: A).(leq g a0 a5))) (\lambda (a4: 
+A).(\lambda (a5: A).(eq A a3 (AHead a4 a5)))) (sc3 g a3 c t) (\lambda (x0: 
+A).(\lambda (x1: A).(\lambda (H8: (leq g a x0)).(\lambda (H9: (leq g a0 
+x1)).(\lambda (H10: (eq A a3 (AHead x0 x1))).(let H11 \def (f_equal A A 
+(\lambda (e: A).e) a3 (AHead x0 x1) H10) in (eq_ind_r A (AHead x0 x1) 
+(\lambda (a4: A).(sc3 g a4 c t)) (conj (arity g c t (AHead x0 x1)) (\forall 
+(d: C).(\forall (w: T).((sc3 g x0 d w) \to (\forall (is: PList).((drop1 is d 
+c) \to (sc3 g x1 d (THead (Flat Appl) w (lift1 is t)))))))) (arity_repl g c t 
+(AHead a a0) H5 (AHead x0 x1) (leq_head g a x0 H8 a0 x1 H9)) (\lambda (d: 
+C).(\lambda (w: T).(\lambda (H12: (sc3 g x0 d w)).(\lambda (is: 
+PList).(\lambda (H13: (drop1 is d c)).(H0 (\lambda (a4: A).(\lambda (H14: 
+(llt a4 a0)).(\lambda (c0: C).(\lambda (t0: T).(\lambda (H15: (sc3 g a4 c0 
+t0)).(\lambda (a5: A).(\lambda (H16: (leq g a4 a5)).(H1 a4 (llt_trans a4 a0 
+(AHead a a0) H14 (llt_head_dx a a0)) c0 t0 H15 a5 H16)))))))) d (THead (Flat 
+Appl) w (lift1 is t)) (H6 d w (H1 x0 (llt_repl g a x0 H8 (AHead a a0) 
+(llt_head_sx a a0)) d w H12 a (leq_sym g a x0 H8)) is H13) x1 H9))))))) a3 
+H11))))))) H7))))) H4)))))))))))) a2)) a1)).
 
 theorem sc3_lift:
  \forall (g: G).(\forall (a: A).(\forall (e: C).(\forall (t: T).((sc3 g a e