(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/leq/props.ma".
+include "Basic-1/leq/props.ma".
theorem asucc_repl:
\forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (leq g
(asucc g a3) (asucc g a4))).(\lambda (a5: A).(\lambda (a6: A).(\lambda (_:
(leq g a5 a6)).(\lambda (H3: (leq g (asucc g a5) (asucc g a6))).(leq_head g
a3 a4 H0 (asucc g a5) (asucc g a6) H3))))))))) a1 a2 H)))).
+(* COMMENTS
+Initial nodes: 1907
+END *)
theorem asucc_inj:
\forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g (asucc g a1) (asucc
in (let H12 \def (eq_ind_r A x0 (\lambda (a5: A).(leq g a a5)) H5 a3 H10) in
(leq_head g a a3 H12 a0 a4 (H0 a4 H11)))))) H8))))))) H4)))))))) a2))))))
a1)).
+(* COMMENTS
+Initial nodes: 4697
+END *)
theorem leq_asucc:
\forall (g: G).(\forall (a: A).(ex A (\lambda (a0: A).(leq g a (asucc g
g x))).(ex_intro A (\lambda (a2: A).(leq g (AHead a0 a1) (asucc g a2)))
(AHead a0 x) (leq_head g a0 a0 (leq_refl g a0) a1 (asucc g x) H2)))) H1))))))
a)).
+(* COMMENTS
+Initial nodes: 221
+END *)
theorem leq_ahead_asucc_false:
\forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g (AHead a1 a2)
H4 (asucc g a0) H7) in (let H10 \def (eq_ind_r A x0 (\lambda (a3: A).(leq g
(AHead a a0) a3)) H3 a H8) in (leq_ahead_false_1 g a a0 H10 P))))) H6)))))))
H2)))))))))) a1)).
+(* COMMENTS
+Initial nodes: 927
+END *)
theorem leq_asucc_false:
\forall (g: G).(\forall (a: A).((leq g (asucc g a) a) \to (\forall (P:
A).(leq g (asucc g a1) a2)) H4 a1 H7) in (let H10 \def (eq_ind_r A x0
(\lambda (a2: A).(leq g a0 a2)) H3 a0 H8) in (H0 H9 P))))) H6)))))))
H2))))))))) a)).
+(* COMMENTS
+Initial nodes: 1327
+END *)