proposition: Lemma FixFun_fix : forall A (R:binary A) B {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) -> F f1 x = F f2 x) -> (forall x, f x = F f x).
proof: Proof. Proof using. intros. apply FixFun_fix_partial with (IB:=IB) (R:=R) (P:=pred_true); auto. hnf; autos*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)