proposition: Lemma leq_gen_induction: forall f (p:EP), (forall x, leq_gen f x x -> (forall y, leq_gen f y x -> y<>x -> p y) -> p x) -> (forall z, leq_gen f z z -> p z).
proof: Proof. ir. cp H0; uh H0. nin H0; ee. apply wo_induction with (a:=x) (p:=p). do 5 (uh H0; ee; try am). ir. assert (leq_gen f x0 x0). rewrite weak_leq_gen_leq with (a:= x). ap leq_refl. do 5 (uh H0; ee; try am). am. am. am. cp (H _ H5). ap H6. ir. assert (leq x y x0). rewrite <- weak_leq_gen_leq with (f := f). am. am. am. ap H4. uh H9; ee; am. uhg; ee; am. uh H2; ee; am. Qed.
imports: Arith order