(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/leq/defs.ma".
+include "Basic-1/leq/defs.ma".
theorem leq_gen_sort1:
\forall (g: G).(\forall (h1: nat).(\forall (n1: nat).(\forall (a2: A).((leq
(aplus g (ASort h2 n2) k))))) (\lambda (n2: nat).(\lambda (h2: nat).(\lambda
(_: nat).(eq A (AHead a3 a5) (ASort h2 n2)))))) H6))))))))))) y a2 H0)))
H))))).
+(* COMMENTS
+Initial nodes: 913
+END *)
theorem leq_gen_head1:
\forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (a: A).((leq g
(a7: A).(leq g a2 a7))) (\lambda (a6: A).(\lambda (a7: A).(eq A (AHead a3 a5)
(AHead a6 a7)))) a3 a5 H12 H10 (refl_equal A (AHead a3 a5)))))))))
H6))))))))))) y a H0))) H))))).
+(* COMMENTS
+Initial nodes: 797
+END *)
theorem leq_gen_sort2:
\forall (g: G).(\forall (h1: nat).(\forall (n1: nat).(\forall (a2: A).((leq
(aplus g (AHead a3 a5) k))))) (\lambda (n2: nat).(\lambda (h2: nat).(\lambda
(_: nat).(eq A (AHead a1 a4) (ASort h2 n2)))))) H6))))))))))) a2 y H0)))
H))))).
+(* COMMENTS
+Initial nodes: 913
+END *)
theorem leq_gen_head2:
\forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (a: A).((leq g a
(a7: A).(leq g a7 a2))) (\lambda (a6: A).(\lambda (a7: A).(eq A (AHead a0 a4)
(AHead a6 a7)))) a0 a4 H12 H10 (refl_equal A (AHead a0 a4)))))))))
H6))))))))))) a y H0))) H))))).
+(* COMMENTS
+Initial nodes: 797
+END *)