proposition: Lemma FixFun2Mod_fix_partial_inv : forall A1 A2 (R:binary (A1*A2)) (P:A1->A2->Prop) B {IB:Inhab B} (S:A1->A2->B->Prop) (E:binary B) F (f:A1->A2->B), f = FixFun2Mod E F -> wf R -> equiv E -> (forall x1 x2, pred_compatible E (S x1 x2)) -> (forall x1 x2 f1 f2, P x1 x2 -> (forall y1 y2, P y1 y2 -> R (y1,y2) (x1,x2) -> E (f1 y1 y2) (f2 y1 y2) /\ S y1 y2 (f1 y1 y2)) -> E (F f1 x1 x2) (F f2 x1 x2) /\ S x1 x2 (F f1 x1 x2)) -> (forall x1 x2, P x1 x2 -> E (f x1 x2) (F f x1 x2)) /\ (forall x1 x2, P x1 x2 -> S x1 x2 (f x1 x2)).
proof: Proof. Proof using. introv Eqf WfR Equiv Comp Cont. sets F': (fun f' => uncurry2 (F (curry2 f'))). forwards~ [H1 H2]: (@FixFunMod_fix_partial_inv (A1*A2)%type R (fun p => P (fst p) (snd p)) B (fun p => S (fst p) (snd p)) IB F' E). intros f1 f2 [x1 x2] Px H. simpls. apply Cont; [assumption|]. intros y1 y2 Py Ryx. apply~ (H (y1,y2)). subst f. split. intros x1 x2 Px. apply~ (H1 (x1,x2)). intros x1 x2 Px. apply~ (H2 (x1,x2)). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)