proposition: Lemma FixFunMod_mixed_partial_inv : forall I A B (M:family I B) (R:binary A) (P:A->Prop) (S:I->A->B->Prop) (E:binary B) {IB:Inhab B} (F:(A->B)->(A->B)) (f:A->B), f = FixFunMod E F -> E = similar M -> COFE M -> wf R -> mixed_continuous M S -> mixed_contractive M P F R S -> (forall x, P x -> E (f x) (F f x)) /\ (forall x i, P x -> S i x (f x)).
proof: Proof. Proof using. introv Deff SimE Cofe Wrr Conti Contr. asserts Equiv: (equiv E). rewrite~ SimE. 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. forwards~ (f&Fixf&Inv): (@mixed_fixed_point _ _ _ _ M E P F R S). lets Fixf': Fixf. rewrite partial_fixed_point_definitions in Fixf'. lets [ED MG]: (Bestg _ Fixf'). forwards [Dom Equ]: ED. eapply mixed_fixed_point_generally_consistent with (R:=R); eauto. clear ED. simpls. split; introv Px. apply~ Fixf. apply* Conti. introv Rji. rewrite SimE in Equ. apply~ Equ. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)