(* This file was automatically generated: do not edit *********************)
-include "Basic-1/csubc/arity.ma".
+include "basic_1/csubc/arity.ma".
-include "Basic-1/csubc/getl.ma".
+include "basic_1/csubc/getl.ma".
-include "Basic-1/csubc/drop1.ma".
+include "basic_1/csubc/drop1.ma".
-include "Basic-1/csubc/props.ma".
+include "basic_1/csubc/props.ma".
-theorem sc3_arity_csubc:
+lemma sc3_arity_csubc:
\forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1
t a) \to (\forall (d1: C).(\forall (is: PList).((drop1 is d1 c1) \to (\forall
(c2: C).((csubc g d1 c2) \to (sc3 g a c2 (lift1 is t)))))))))))
x2))).(\lambda (_: (csubc g x x1)).(\lambda (_: (sc3 g (asucc g x3) x (lift1
(ptrans is i) u))).(\lambda (_: (sc3 g x3 x1 x2)).(let H18 \def (eq_ind C x0
(\lambda (c0: C).(getl (trans is i) c2 c0)) H9 (CHead x1 (Bind Abbr) x2) H14)
-in (let H19 \def (eq_ind K (Bind Abbr) (\lambda (ee: K).(match ee in K return
-(\lambda (_: K).Prop) with [(Bind b) \Rightarrow (match b in B return
-(\lambda (_: B).Prop) with [Abbr \Rightarrow True | Abst \Rightarrow False |
-Void \Rightarrow False]) | (Flat _) \Rightarrow False])) I (Bind Abst) H13)
+in (let H19 \def (eq_ind K (Bind Abbr) (\lambda (ee: K).(match ee with [(Bind
+b) \Rightarrow (match b with [Abbr \Rightarrow True | Abst \Rightarrow False
+| Void \Rightarrow False]) | (Flat _) \Rightarrow False])) I (Bind Abst) H13)
in (False_ind (sc3 g a0 c2 (lift1 is (TLRef i))) H19))))))))))) H12))
(\lambda (H12: (ex4_3 B C T (\lambda (b: B).(\lambda (c3: C).(\lambda (v2:
T).(eq C x0 (CHead c3 (Bind b) v2))))) (\lambda (_: B).(\lambda (_:
K (Bind Abbr) (Bind Void))).(\lambda (_: (not (eq B x1 Void))).(\lambda (_:
(csubc g x x2)).(let H17 \def (eq_ind C x0 (\lambda (c0: C).(getl (trans is
i) c2 c0)) H9 (CHead x2 (Bind x1) x3) H13) in (let H18 \def (eq_ind K (Bind
-Abbr) (\lambda (ee: K).(match ee in K return (\lambda (_: K).Prop) with
-[(Bind b) \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr
-\Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat
-_) \Rightarrow False])) I (Bind Void) H14) in (False_ind (sc3 g a0 c2 (lift1
-is (TLRef i))) H18)))))))))) H12)) H11)))))) H8)))))) H5))))))))))))))))
-(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
-(H0: (getl i c (CHead d (Bind Abst) u))).(\lambda (a0: A).(\lambda (H1:
-(arity g d u (asucc g a0))).(\lambda (_: ((\forall (d1: C).(\forall (is:
-PList).((drop1 is d1 d) \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g
-(asucc g a0) c2 (lift1 is u))))))))).(\lambda (d1: C).(\lambda (is:
-PList).(\lambda (H3: (drop1 is d1 c)).(\lambda (c2: C).(\lambda (H4: (csubc g
-d1 c2)).(let H5 \def H0 in (let H_x \def (drop1_getl_trans is c d1 H3 Abst d
-u i H5) in (let H6 \def H_x in (ex2_ind C (\lambda (e2: C).(drop1 (ptrans is
-i) e2 d)) (\lambda (e2: C).(getl (trans is i) d1 (CHead e2 (Bind Abst) (lift1
-(ptrans is i) u)))) (sc3 g a0 c2 (lift1 is (TLRef i))) (\lambda (x:
-C).(\lambda (H7: (drop1 (ptrans is i) x d)).(\lambda (H8: (getl (trans is i)
-d1 (CHead x (Bind Abst) (lift1 (ptrans is i) u)))).(let H_x0 \def
+Abbr) (\lambda (ee: K).(match ee with [(Bind b) \Rightarrow (match b with
+[Abbr \Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False]) |
+(Flat _) \Rightarrow False])) I (Bind Void) H14) in (False_ind (sc3 g a0 c2
+(lift1 is (TLRef i))) H18)))))))))) H12)) H11)))))) H8))))))
+H5)))))))))))))))) (\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda
+(i: nat).(\lambda (H0: (getl i c (CHead d (Bind Abst) u))).(\lambda (a0:
+A).(\lambda (H1: (arity g d u (asucc g a0))).(\lambda (_: ((\forall (d1:
+C).(\forall (is: PList).((drop1 is d1 d) \to (\forall (c2: C).((csubc g d1
+c2) \to (sc3 g (asucc g a0) c2 (lift1 is u))))))))).(\lambda (d1: C).(\lambda
+(is: PList).(\lambda (H3: (drop1 is d1 c)).(\lambda (c2: C).(\lambda (H4:
+(csubc g d1 c2)).(let H5 \def H0 in (let H_x \def (drop1_getl_trans is c d1
+H3 Abst d u i H5) in (let H6 \def H_x in (ex2_ind C (\lambda (e2: C).(drop1
+(ptrans is i) e2 d)) (\lambda (e2: C).(getl (trans is i) d1 (CHead e2 (Bind
+Abst) (lift1 (ptrans is i) u)))) (sc3 g a0 c2 (lift1 is (TLRef i))) (\lambda
+(x: C).(\lambda (H7: (drop1 (ptrans is i) x d)).(\lambda (H8: (getl (trans is
+i) d1 (CHead x (Bind Abst) (lift1 (ptrans is i) u)))).(let H_x0 \def
(csubc_getl_conf g d1 (CHead x (Bind Abst) (lift1 (ptrans is i) u)) (trans is
i) H8 c2 H4) in (let H9 \def H_x0 in (ex2_ind C (\lambda (e2: C).(getl (trans
is i) c2 e2)) (\lambda (e2: C).(csubc g (CHead x (Bind Abst) (lift1 (ptrans
K (Bind Abst) (Bind Void))).(\lambda (_: (not (eq B x1 Void))).(\lambda (_:
(csubc g x x2)).(let H18 \def (eq_ind C x0 (\lambda (c0: C).(getl (trans is
i) c2 c0)) H10 (CHead x2 (Bind x1) x3) H14) in (let H19 \def (eq_ind K (Bind
-Abst) (\lambda (ee: K).(match ee in K return (\lambda (_: K).Prop) with
-[(Bind b) \Rightarrow (match b in B return (\lambda (_: B).Prop) with [Abbr
-\Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat
-_) \Rightarrow False])) I (Bind Void) H15) in (False_ind (sc3 g a0 c2 (lift1
-is (TLRef i))) H19)))))))))) H13)) H12)))))) H9)))))) H6)))))))))))))))))
-(\lambda (b: B).(\lambda (H0: (not (eq B b Abst))).(\lambda (c: C).(\lambda
-(u: T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H2:
-((\forall (d1: C).(\forall (is: PList).((drop1 is d1 c) \to (\forall (c2:
-C).((csubc g d1 c2) \to (sc3 g a1 c2 (lift1 is u))))))))).(\lambda (t0:
-T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c (Bind b) u) t0
-a2)).(\lambda (H4: ((\forall (d1: C).(\forall (is: PList).((drop1 is d1
-(CHead c (Bind b) u)) \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g a2 c2
-(lift1 is t0))))))))).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H5:
-(drop1 is d1 c)).(\lambda (c2: C).(\lambda (H6: (csubc g d1 c2)).(let H_y
-\def (sc3_bind g b H0 a1 a2 TNil) in (eq_ind_r T (THead (Bind b) (lift1 is u)
-(lift1 (Ss is) t0)) (\lambda (t1: T).(sc3 g a2 c2 t1)) (H_y c2 (lift1 is u)
-(lift1 (Ss is) t0) (H4 (CHead d1 (Bind b) (lift1 is u)) (Ss is)
-(drop1_skip_bind b c is d1 u H5) (CHead c2 (Bind b) (lift1 is u)) (csubc_head
-g d1 c2 H6 (Bind b) (lift1 is u))) (H2 d1 is H5 c2 H6)) (lift1 is (THead
-(Bind b) u t0)) (lift1_bind b is u t0))))))))))))))))))) (\lambda (c:
+Abst) (\lambda (ee: K).(match ee with [(Bind b) \Rightarrow (match b with
+[Abbr \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) |
+(Flat _) \Rightarrow False])) I (Bind Void) H15) in (False_ind (sc3 g a0 c2
+(lift1 is (TLRef i))) H19)))))))))) H13)) H12)))))) H9))))))
+H6))))))))))))))))) (\lambda (b: B).(\lambda (H0: (not (eq B b
+Abst))).(\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity
+g c u a1)).(\lambda (H2: ((\forall (d1: C).(\forall (is: PList).((drop1 is d1
+c) \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g a1 c2 (lift1 is
+u))))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c
+(Bind b) u) t0 a2)).(\lambda (H4: ((\forall (d1: C).(\forall (is:
+PList).((drop1 is d1 (CHead c (Bind b) u)) \to (\forall (c2: C).((csubc g d1
+c2) \to (sc3 g a2 c2 (lift1 is t0))))))))).(\lambda (d1: C).(\lambda (is:
+PList).(\lambda (H5: (drop1 is d1 c)).(\lambda (c2: C).(\lambda (H6: (csubc g
+d1 c2)).(let H_y \def (sc3_bind g b H0 a1 a2 TNil) in (eq_ind_r T (THead
+(Bind b) (lift1 is u) (lift1 (Ss is) t0)) (\lambda (t1: T).(sc3 g a2 c2 t1))
+(H_y c2 (lift1 is u) (lift1 (Ss is) t0) (H4 (CHead d1 (Bind b) (lift1 is u))
+(Ss is) (drop1_skip_bind b c is d1 u H5) (CHead c2 (Bind b) (lift1 is u))
+(csubc_head g d1 c2 H6 (Bind b) (lift1 is u))) (H2 d1 is H5 c2 H6)) (lift1 is
+(THead (Bind b) u t0)) (lift1_bind b is u t0))))))))))))))))))) (\lambda (c:
C).(\lambda (u: T).(\lambda (a1: A).(\lambda (H0: (arity g c u (asucc g
a1))).(\lambda (H1: ((\forall (d1: C).(\forall (is: PList).((drop1 is d1 c)
\to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g (asucc g a1) c2 (lift1 is
is0 (lift1 is u)) (lift1 (Ss is0) (lift1 (Ss is) t0))) (\lambda (t1: T).(sc3
g a2 d (THead (Flat Appl) w t1))) (let H8 \def (sc3_appl g a1 a2 TNil) in (H8
d w (lift1 (Ss is0) (lift1 (Ss is) t0)) (let H_y \def (sc3_bind g Abbr
-(\lambda (H9: (eq B Abbr Abst)).(not_abbr_abst H9)) a1 a2 TNil) in (H_y d w
-(lift1 (Ss is0) (lift1 (Ss is) t0)) (let H_x \def (csubc_drop1_conf_rev g is0
-d c2 H7 d1 H5) in (let H9 \def H_x in (ex2_ind C (\lambda (c3: C).(drop1 is0
-c3 d1)) (\lambda (c3: C).(csubc g c3 d)) (sc3 g a2 (CHead d (Bind Abbr) w)
-(lift1 (Ss is0) (lift1 (Ss is) t0))) (\lambda (x: C).(\lambda (H10: (drop1
-is0 x d1)).(\lambda (H11: (csubc g x d)).(eq_ind_r T (lift1 (papp (Ss is0)
-(Ss is)) t0) (\lambda (t1: T).(sc3 g a2 (CHead d (Bind Abbr) w) t1))
-(eq_ind_r PList (Ss (papp is0 is)) (\lambda (p: PList).(sc3 g a2 (CHead d
-(Bind Abbr) w) (lift1 p t0))) (H3 (CHead x (Bind Abst) (lift1 (papp is0 is)
-u)) (Ss (papp is0 is)) (drop1_skip_bind Abst c (papp is0 is) x u (drop1_trans
-is0 x d1 H10 is c H4)) (CHead d (Bind Abbr) w) (csubc_abst g x d H11 (lift1
-(papp is0 is) u) a1 (H1 x (papp is0 is) (drop1_trans is0 x d1 H10 is c H4) x
-(csubc_refl g x)) w H6)) (papp (Ss is0) (Ss is)) (papp_ss is0 is)) (lift1 (Ss
-is0) (lift1 (Ss is) t0)) (lift1_lift1 (Ss is0) (Ss is) t0))))) H9))) H6)) H6
-(lift1 is0 (lift1 is u)) (sc3_lift1 g c2 (asucc g a1) is0 d (lift1 is u) (H1
-d1 is H4 c2 H5) H7))) (lift1 is0 (THead (Bind Abst) (lift1 is u) (lift1 (Ss
-is) t0))) (lift1_bind Abst is0 (lift1 is u) (lift1 (Ss is) t0))))))))) (lift1
-is (THead (Bind Abst) u t0)) (lift1_bind Abst is u t0))))))))))))))))
-(\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u
-a1)).(\lambda (H1: ((\forall (d1: C).(\forall (is: PList).((drop1 is d1 c)
-\to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g a1 c2 (lift1 is
-u))))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g c t0
-(AHead a1 a2))).(\lambda (H3: ((\forall (d1: C).(\forall (is: PList).((drop1
-is d1 c) \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g (AHead a1 a2) c2
-(lift1 is t0))))))))).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H4:
-(drop1 is d1 c)).(\lambda (c2: C).(\lambda (H5: (csubc g d1 c2)).(let H_y
-\def (H1 d1 is H4 c2 H5) in (let H_y0 \def (H3 d1 is H4 c2 H5) in (let H6
-\def H_y0 in (land_ind (arity g c2 (lift1 is t0) (AHead a1 a2)) (\forall (d:
-C).(\forall (w: T).((sc3 g a1 d w) \to (\forall (is0: PList).((drop1 is0 d
-c2) \to (sc3 g a2 d (THead (Flat Appl) w (lift1 is0 (lift1 is t0)))))))))
-(sc3 g a2 c2 (lift1 is (THead (Flat Appl) u t0))) (\lambda (_: (arity g c2
-(lift1 is t0) (AHead a1 a2))).(\lambda (H8: ((\forall (d: C).(\forall (w:
-T).((sc3 g a1 d w) \to (\forall (is0: PList).((drop1 is0 d c2) \to (sc3 g a2
-d (THead (Flat Appl) w (lift1 is0 (lift1 is t0))))))))))).(let H_y1 \def (H8
-c2 (lift1 is u) H_y PNil) in (eq_ind_r T (THead (Flat Appl) (lift1 is u)
-(lift1 is t0)) (\lambda (t1: T).(sc3 g a2 c2 t1)) (H_y1 (drop1_nil c2))
-(lift1 is (THead (Flat Appl) u t0)) (lift1_flat Appl is u t0)))))
-H6)))))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a0:
-A).(\lambda (_: (arity g c u (asucc g a0))).(\lambda (H1: ((\forall (d1:
-C).(\forall (is: PList).((drop1 is d1 c) \to (\forall (c2: C).((csubc g d1
-c2) \to (sc3 g (asucc g a0) c2 (lift1 is u))))))))).(\lambda (t0: T).(\lambda
-(_: (arity g c t0 a0)).(\lambda (H3: ((\forall (d1: C).(\forall (is:
-PList).((drop1 is d1 c) \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g a0
-c2 (lift1 is t0))))))))).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H4:
-(drop1 is d1 c)).(\lambda (c2: C).(\lambda (H5: (csubc g d1 c2)).(let H_y
-\def (sc3_cast g a0 TNil) in (eq_ind_r T (THead (Flat Cast) (lift1 is u)
-(lift1 is t0)) (\lambda (t1: T).(sc3 g a0 c2 t1)) (H_y c2 (lift1 is u) (H1 d1
-is H4 c2 H5) (lift1 is t0) (H3 d1 is H4 c2 H5)) (lift1 is (THead (Flat Cast)
-u t0)) (lift1_flat Cast is u t0)))))))))))))))) (\lambda (c: C).(\lambda (t0:
-T).(\lambda (a1: A).(\lambda (_: (arity g c t0 a1)).(\lambda (H1: ((\forall
+not_abbr_abst a1 a2 TNil) in (H_y d w (lift1 (Ss is0) (lift1 (Ss is) t0))
+(let H_x \def (csubc_drop1_conf_rev g is0 d c2 H7 d1 H5) in (let H9 \def H_x
+in (ex2_ind C (\lambda (c3: C).(drop1 is0 c3 d1)) (\lambda (c3: C).(csubc g
+c3 d)) (sc3 g a2 (CHead d (Bind Abbr) w) (lift1 (Ss is0) (lift1 (Ss is) t0)))
+(\lambda (x: C).(\lambda (H10: (drop1 is0 x d1)).(\lambda (H11: (csubc g x
+d)).(eq_ind_r T (lift1 (papp (Ss is0) (Ss is)) t0) (\lambda (t1: T).(sc3 g a2
+(CHead d (Bind Abbr) w) t1)) (eq_ind_r PList (Ss (papp is0 is)) (\lambda (p:
+PList).(sc3 g a2 (CHead d (Bind Abbr) w) (lift1 p t0))) (H3 (CHead x (Bind
+Abst) (lift1 (papp is0 is) u)) (Ss (papp is0 is)) (drop1_skip_bind Abst c
+(papp is0 is) x u (drop1_trans is0 x d1 H10 is c H4)) (CHead d (Bind Abbr) w)
+(csubc_abst g x d H11 (lift1 (papp is0 is) u) a1 (H1 x (papp is0 is)
+(drop1_trans is0 x d1 H10 is c H4) x (csubc_refl g x)) w H6)) (papp (Ss is0)
+(Ss is)) (papp_ss is0 is)) (lift1 (Ss is0) (lift1 (Ss is) t0)) (lift1_lift1
+(Ss is0) (Ss is) t0))))) H9))) H6)) H6 (lift1 is0 (lift1 is u)) (sc3_lift1 g
+c2 (asucc g a1) is0 d (lift1 is u) (H1 d1 is H4 c2 H5) H7))) (lift1 is0
+(THead (Bind Abst) (lift1 is u) (lift1 (Ss is) t0))) (lift1_bind Abst is0
+(lift1 is u) (lift1 (Ss is) t0))))))))) (lift1 is (THead (Bind Abst) u t0))
+(lift1_bind Abst is u t0)))))))))))))))) (\lambda (c: C).(\lambda (u:
+T).(\lambda (a1: A).(\lambda (_: (arity g c u a1)).(\lambda (H1: ((\forall
(d1: C).(\forall (is: PList).((drop1 is d1 c) \to (\forall (c2: C).((csubc g
-d1 c2) \to (sc3 g a1 c2 (lift1 is t0))))))))).(\lambda (a2: A).(\lambda (H2:
-(leq g a1 a2)).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H3: (drop1 is
-d1 c)).(\lambda (c2: C).(\lambda (H4: (csubc g d1 c2)).(sc3_repl g a1 c2
-(lift1 is t0) (H1 d1 is H3 c2 H4) a2 H2))))))))))))) c1 t a H))))).
-(* COMMENTS
-Initial nodes: 5940
-END *)
+d1 c2) \to (sc3 g a1 c2 (lift1 is u))))))))).(\lambda (t0: T).(\lambda (a2:
+A).(\lambda (_: (arity g c t0 (AHead a1 a2))).(\lambda (H3: ((\forall (d1:
+C).(\forall (is: PList).((drop1 is d1 c) \to (\forall (c2: C).((csubc g d1
+c2) \to (sc3 g (AHead a1 a2) c2 (lift1 is t0))))))))).(\lambda (d1:
+C).(\lambda (is: PList).(\lambda (H4: (drop1 is d1 c)).(\lambda (c2:
+C).(\lambda (H5: (csubc g d1 c2)).(let H_y \def (H1 d1 is H4 c2 H5) in (let
+H_y0 \def (H3 d1 is H4 c2 H5) in (let H6 \def H_y0 in (land_ind (arity g c2
+(lift1 is t0) (AHead a1 a2)) (\forall (d: C).(\forall (w: T).((sc3 g a1 d w)
+\to (\forall (is0: PList).((drop1 is0 d c2) \to (sc3 g a2 d (THead (Flat
+Appl) w (lift1 is0 (lift1 is t0))))))))) (sc3 g a2 c2 (lift1 is (THead (Flat
+Appl) u t0))) (\lambda (_: (arity g c2 (lift1 is t0) (AHead a1 a2))).(\lambda
+(H8: ((\forall (d: C).(\forall (w: T).((sc3 g a1 d w) \to (\forall (is0:
+PList).((drop1 is0 d c2) \to (sc3 g a2 d (THead (Flat Appl) w (lift1 is0
+(lift1 is t0))))))))))).(let H_y1 \def (H8 c2 (lift1 is u) H_y PNil) in
+(eq_ind_r T (THead (Flat Appl) (lift1 is u) (lift1 is t0)) (\lambda (t1:
+T).(sc3 g a2 c2 t1)) (H_y1 (drop1_nil c2)) (lift1 is (THead (Flat Appl) u
+t0)) (lift1_flat Appl is u t0))))) H6)))))))))))))))))) (\lambda (c:
+C).(\lambda (u: T).(\lambda (a0: A).(\lambda (_: (arity g c u (asucc g
+a0))).(\lambda (H1: ((\forall (d1: C).(\forall (is: PList).((drop1 is d1 c)
+\to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g (asucc g a0) c2 (lift1 is
+u))))))))).(\lambda (t0: T).(\lambda (_: (arity g c t0 a0)).(\lambda (H3:
+((\forall (d1: C).(\forall (is: PList).((drop1 is d1 c) \to (\forall (c2:
+C).((csubc g d1 c2) \to (sc3 g a0 c2 (lift1 is t0))))))))).(\lambda (d1:
+C).(\lambda (is: PList).(\lambda (H4: (drop1 is d1 c)).(\lambda (c2:
+C).(\lambda (H5: (csubc g d1 c2)).(let H_y \def (sc3_cast g a0 TNil) in
+(eq_ind_r T (THead (Flat Cast) (lift1 is u) (lift1 is t0)) (\lambda (t1:
+T).(sc3 g a0 c2 t1)) (H_y c2 (lift1 is u) (H1 d1 is H4 c2 H5) (lift1 is t0)
+(H3 d1 is H4 c2 H5)) (lift1 is (THead (Flat Cast) u t0)) (lift1_flat Cast is
+u t0)))))))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (a1:
+A).(\lambda (_: (arity g c t0 a1)).(\lambda (H1: ((\forall (d1: C).(\forall
+(is: PList).((drop1 is d1 c) \to (\forall (c2: C).((csubc g d1 c2) \to (sc3 g
+a1 c2 (lift1 is t0))))))))).(\lambda (a2: A).(\lambda (H2: (leq g a1
+a2)).(\lambda (d1: C).(\lambda (is: PList).(\lambda (H3: (drop1 is d1
+c)).(\lambda (c2: C).(\lambda (H4: (csubc g d1 c2)).(sc3_repl g a1 c2 (lift1
+is t0) (H1 d1 is H3 c2 H4) a2 H2))))))))))))) c1 t a H))))).
-theorem sc3_arity:
+lemma sc3_arity:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
a) \to (sc3 g a c t)))))
\def
\lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (a: A).(\lambda (H:
(arity g c t a)).(let H_y \def (sc3_arity_csubc g c t a H c PNil) in (H_y
(drop1_nil c) c (csubc_refl g c))))))).
-(* COMMENTS
-Initial nodes: 47
-END *)
projects / helm.git / blobdiff