proposition: Lemma FixFun_fix_partial_inv : forall A (R:binary A) (P:A->Prop) B (S:A->B->Prop) {IB:Inhab B} (F:(A->B)->(A->B)) (f:A->B), f = FixFun F -> wf R -> rec_contractive eq P F R S -> (forall x, P x -> f x = F f x) /\ (forall x, P x -> S x (f x)).
proof: Proof. Proof using. intros. applys* (@FixFunMod_fix_partial_inv A R). intros_all. subst~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)