(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/ty3/pr3_props.ma".
+include "Basic-1/ty3/pr3_props.ma".
-include "LambdaDelta-1/arity/pr3.ma".
+include "Basic-1/arity/pr3.ma".
-include "LambdaDelta-1/asucc/fwd.ma".
+include "Basic-1/asucc/fwd.ma".
theorem ty3_arity:
\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c
x) (arity_repl g c0 t0 (asucc g x0) H9 (asucc g (asucc g x)) (asucc_repl g x0
(asucc g x) (arity_mono g c0 t4 x0 H8 (asucc g x) H6))) t4 H6))))) H7)))))
H4)))))))))) c t1 t2 H))))).
+(* COMMENTS
+Initial nodes: 3761
+END *)