(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/asucc/defs.ma".
+include "Basic-1/asucc/defs.ma".
theorem asucc_gen_sort:
\forall (g: G).(\forall (h: nat).(\forall (n: nat).(\forall (a: A).((eq A
False])) I (asucc g (AHead a0 a1)) H1) in (False_ind (ex_2 nat nat (\lambda
(h0: nat).(\lambda (n0: nat).(eq A (AHead a0 a1) (ASort h0 n0))))) H2)))))))
a)))).
+(* COMMENTS
+Initial nodes: 317
+END *)
theorem asucc_gen_head:
\forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (a: A).((eq A
a1 a3) (AHead a1 a4))) (\lambda (a4: A).(eq A (asucc g a3) (asucc g a4))) a3
(refl_equal A (AHead a1 a3)) (refl_equal A (asucc g a3))) a2 H3))) a0 H4))))
H2))))))) a)))).
+(* COMMENTS
+Initial nodes: 957
+END *)