proposition: Lemma FixFun_fix_partial' : forall A (R:binary A) (P:A->Prop) B {IB:Inhab B} (F:(A->B)->(A->B)) (f' f:A->B), f = FixFun F -> wf R -> rec_contractive' eq P F R f' -> fixed_point (pfun_equal P) F f' -> (forall x, P x -> f x = F f x).
proof: Proof. Proof using. introv Df W Cont Fixf'. applys Fixf' (Build_partial f P). simpl. applys~ FixFunMod_inv F. applys~ rec_fixed_point_generally_consistent' R. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)