(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/arity/props.ma".
+include "Basic-1/arity/props.ma".
-include "LambdaDelta-1/arity/cimp.ma".
+include "Basic-1/arity/cimp.ma".
-include "LambdaDelta-1/aprem/props.ma".
+include "Basic-1/aprem/props.ma".
theorem arity_aprem:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
T).(\lambda (_: nat).(arity g d u (asucc g b))))) x0 x1 x2 H8 (arity_repl g
x0 x1 (asucc g x) H9 (asucc g b) (asucc_repl g x b H5)))))))) H7))))))
H4))))))))))))) c t a H))))).
+(* COMMENTS
+Initial nodes: 4526
+END *)