proposition: Lemma lfp_ind (P : A -> Prop) : Proper (eq ==> impl) P -> (forall x, P x -> P (f x)) -> (forall S, S [<=] P -> P (lub S)) -> P lfp.
proof: Proof. intros Peq Pf Plub. rewrite <- lfp_eq_lub. apply Plub. induction 1. apply Pf. hyp. apply Plub. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SetUtil) Coq(Morphisms Basics)