(* This file was automatically generated: do not edit *********************)
-
-
-include "arity/fwd.ma".
+include "LambdaDelta-1/arity/fwd.ma".
theorem node_inh:
\forall (g: G).(\forall (n: nat).(\forall (k: nat).(ex_2 C T (\lambda (c:
(t0: T).(\lambda (_: (arity g c0 t0 a)).(\lambda (H3: ((\forall (a2:
A).((arity g c0 t0 a2) \to (leq g a a2))))).(\lambda (a2: A).(\lambda (H4:
(arity g c0 (THead (Flat Cast) u t0) a2)).(let H5 \def (arity_gen_cast g c0 u
-t0 a2 H4) in (and_ind (arity g c0 u (asucc g a2)) (arity g c0 t0 a2) (leq g a
-a2) (\lambda (_: (arity g c0 u (asucc g a2))).(\lambda (H7: (arity g c0 t0
+t0 a2 H4) in (land_ind (arity g c0 u (asucc g a2)) (arity g c0 t0 a2) (leq g
+a a2) (\lambda (_: (arity g c0 u (asucc g a2))).(\lambda (H7: (arity g c0 t0
a2)).(H3 a2 H7))) H5)))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda
(a2: A).(\lambda (_: (arity g c0 t0 a2)).(\lambda (H1: ((\forall (a3:
A).((arity g c0 t0 a3) \to (leq g a2 a3))))).(\lambda (a3: A).(\lambda (H2: