(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/arity/props.ma".
+include "Basic-1/arity/props.ma".
-include "LambdaDelta-1/fsubst0/fwd.ma".
+include "Basic-1/fsubst0/fwd.ma".
-include "LambdaDelta-1/csubst0/getl.ma".
+include "Basic-1/csubst0/getl.ma".
-include "LambdaDelta-1/subst0/dec.ma".
+include "Basic-1/subst0/dec.ma".
-include "LambdaDelta-1/subst0/fwd.ma".
+include "Basic-1/subst0/fwd.ma".
-include "LambdaDelta-1/getl/getl.ma".
+include "Basic-1/getl/getl.ma".
theorem arity_gen_cvoid_subst0:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
nat).(\lambda (H3: (getl i c0 (CHead d (Bind Void) u))).(\lambda (w:
T).(\lambda (v: T).(\lambda (H4: (subst0 i w t0 v)).(\lambda (P: Prop).(H1 d
u i H3 w v H4 P)))))))))))))))) c t a H))))).
+(* COMMENTS
+Initial nodes: 4131
+END *)
theorem arity_gen_cvoid:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
x) (\lambda (t0: T).(ex T (\lambda (v: T).(eq T t0 (lift (S O) i v)))))
(ex_intro T (\lambda (v: T).(eq T (lift (S O) i x) (lift (S O) i v))) x
(refl_equal T (lift (S O) i x))) t H3))) H2))) H1))))))))))).
+(* COMMENTS
+Initial nodes: 423
+END *)
theorem arity_fsubst0:
\forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (a: A).((arity g
(\lambda (H7: (subst0 i u t t2)).(\lambda (H8: (csubst0 i u c
c2)).(arity_repl g c2 t2 a1 (H1 d1 u i H3 c2 t2 (fsubst0_both i u c t t2 H7
c2 H8)) a2 H2))) H6)) H5))))))))))))))))) c1 t1 a H))))).
+(* COMMENTS
+Initial nodes: 20387
+END *)
theorem arity_subst0:
\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (a: A).((arity g c
(H0: (getl i c (CHead d (Bind Abbr) u))).(\lambda (t2: T).(\lambda (H1:
(subst0 i u t1 t2)).(arity_fsubst0 g c t1 a H d u i H0 c t2 (fsubst0_snd i u
c t1 t2 H1)))))))))))).
+(* COMMENTS
+Initial nodes: 89
+END *)