proposition: Lemma FixFun2_fix : forall A1 A2 (R:binary (A1*A2)) B {IB:Inhab B} F (f:A1->A2->B), f = FixFun2 F -> wf R -> (forall x1 x2 f1 f2, (forall y1 y2, R (y1,y2) (x1,x2) -> f1 y1 y2 = f2 y1 y2) -> F f1 x1 x2 = F f2 x1 x2) -> (forall x1 x2, f x1 x2 = F f x1 x2).
proof: Proof. Proof using. intros. applys* (FixFun2_fix_partial R (fun _ _ => True)). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)