proposition: Lemma FixFun_fix_inv : forall A (R:binary A) B (S:A->B->Prop) {IB:Inhab B} (F:(A->B)->(A->B)) (f:A->B), f = FixFun F -> wf R -> (forall f1 f2 x, (forall y, R y x -> (f1 y) = (f2 y) /\ S y (f1 y)) -> (F f1 x) = (F f2 x) /\ S x (F f1 x)) -> (forall x, f x = F f x) /\ (forall x, S x (f x)).
proof: Proof. Proof using. intros. forwards~ [K1 K2]: (FixFun_fix_partial_inv R pred_true S). subst~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)