proposition: Lemma FixFunMod_inv : forall A (P:A->Prop) B {IB:Inhab B} (F:(A->B)->(A->B)) (E:binary B) (f f':A->B), f = FixFunMod E F -> equiv E -> generally_consistent_partial_fixed_point E F (Build_partial f' P) -> pfun_equiv E P f' f.
proof: Proof. Proof using. introv Deff Equiv Gcf'. unfolds FixFunMod, Fix. epsilon g. forwards* [g Opt]: (@optimal_fixed_point_exists _ _ _ E F). exists g. apply~ Fix_prop_of_optimal. intros [Fixg Bestg]. subst f. lets Fixf: (proj1 Gcf'). rewrite partial_fixed_point_definitions in Fixf. lets [ED MG]: (Bestg _ Fixf). forwards~ [Dom Equ]: ED. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)