proposition: Lemma FixFun2_fix_partial_inv : forall A1 A2 (R:binary (A1*A2)) (P:A1->A2->Prop) B (S:A1->A2->B->Prop) {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 /\ S y1 y2 (f1 y1 y2)) -> F f1 x1 x2 = F f2 x1 x2 /\ S x1 x2 (F f1 x1 x2)) -> (forall x1 x2, P x1 x2 -> f x1 x2 = F f x1 x2) /\ (forall x1 x2, P x1 x2 -> S x1 x2 (f x1 x2)).
proof: Proof. Proof using. intros. eapply FixFun2Mod_fix_partial with (E:=eq) (R:=R); autos~. intros_all. subst~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)