proposition: Lemma FixFunMod_mixed_partial : forall I A B (M:family I B) (R:binary A) (P:A->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_contractive_noinv M P F R -> (forall x, P x -> E (f x) (F f x)).
proof: Proof. Proof using. introv Def Equiv Cofe Wf Trans Cont. forwards~ [H _]: (@FixFunMod_mixed_partial_inv I A B M R P (fun _ _ _ => True) E IB F f Def). apply~ mixed_contractive_noinv_to_mixed_contractive. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)