(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/ty3/arity.ma".
+include "Basic-1/ty3/arity.ma".
theorem csubt_csuba:
\forall (g: G).(\forall (c1: C).(\forall (c2: C).((csubt g c1 c2) \to (csuba
(x: A).(\lambda (H5: (arity g c3 u x)).(\lambda (H6: (arity g c3 t (asucc g
x))).(csuba_abst g c3 c4 H1 t x H6 u (csuba_arity g c3 u x H5 c4 H1)))))
H4))))))))))) c1 c2 H)))).
+(* COMMENTS
+Initial nodes: 313
+END *)