proposition: Lemma partial_fixed_point_definitions' A B F (f:A-->B) (E:binary B) : partial_fixed_point E F f <-> forall (f':A-->B), pfun_equiv E (dom f) f f' -> pfun_equiv E (dom f) f' (F f').
proof: Proof. Proof using. split; intros Fixf f' Eff'. apply~ Fixf. apply~ (Fixf (Build_partial f' (dom f))). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)