(* 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
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:
(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
projects / helm.git / blobdiff