proposition: Lemma FixFunMod_fix_partial : forall A (R:binary A) (P:A->Prop) B {IB:Inhab B} (F:(A->B)->(A->B)) (E:binary B) (f:A->B), f = FixFunMod E F -> equiv E -> wf R -> rec_contractive_noinv E P F R -> (forall x, P x -> E (f x) (F f x)).
proof: Proof. Proof using. introv Def Equiv Wf Cont. forwards~ [H _]: (@FixFunMod_fix_partial_inv A R P B post_true IB F E f Def). apply~ rec_contractive_noinv_to_rec_contractive. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)