proposition: Lemma FixFun2_fix_partial : forall A1 A2 (R:binary (A1*A2)) (P:A1->A2->Prop) B {IB:Inhab B} F (f:A1->A2->B), f = FixFun2 F -> wf R -> (forall x1 x2 f1 f2, P x1 x2 -> (forall y1 y2, P y1 y2 -> R (y1,y2) (x1,x2) -> f1 y1 y2 = f2 y1 y2) -> F f1 x1 x2 = F f2 x1 x2) -> (forall x1 x2, P x1 x2 -> f x1 x2 = F f x1 x2).
proof: Proof. Proof using. intros. forwards [K _]: (@FixFun2_fix_partial_inv A1 A2 R P B (fun _ _ _ => True) _ F); autos~. intros_all. split~. applys~ H1 f1 f2. intros. forwards*: H4. subst~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)