proposition: Lemma gfp_ext : forall f g, (forall x, f x == g x) -> gfp f == gfp g.
proof: Proof. intros f g fg. unfold lfp. apply lub_equiv. intro x. unfold mem. rewrite fg. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SetUtil) Coq(Morphisms Basics)