(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/csubc/arity.ma".
+include "Basic-1/csubc/arity.ma".
-include "LambdaDelta-1/csubc/getl.ma".
+include "Basic-1/csubc/getl.ma".
-include "LambdaDelta-1/csubc/drop1.ma".
+include "Basic-1/csubc/drop1.ma".
-include "LambdaDelta-1/csubc/props.ma".
+include "Basic-1/csubc/props.ma".
theorem sc3_arity_csubc:
\forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).((arity g c1
(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 *)
theorem sc3_arity:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
\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 *)