include "LambdaDelta-1/aprem/props.ma".
-include "LambdaDelta-1/aprem/fwd.ma".
-
theorem arity_aprem:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((arity g c t
a) \to (\forall (i: nat).(\forall (b: A).((aprem i a b) \to (ex2_3 C T nat