proposition: Lemma FixFun2Mod_corec : forall I A1 A2 B (M:family I B) {IB:Inhab B} (E:binary B) F (f:A1->A2->B), f = FixFun2Mod E F -> E = similar M -> COFE M -> (forall i x1 x2 f1 f2, (forall j y1 y2, family_r M j i -> family_sim M j (f1 y1 y2) (f2 y1 y2)) -> family_sim M i (F f1 x1 x2) (F f2 x1 x2)) -> forall x1 x2, E (f x1 x2) (F f x1 x2).
proof: Proof. Proof using. introv Eqf Esim Cofe Cont. sets F': (fun f' => uncurry2 (F (curry2 f'))). forwards~ [H1 H2]: (@FixFunMod_corec_inv I (A1*A2)%type B M (fun _ => True) (fun _ _ => True) IB E F'). intros i [x1 x2] f1 f2 Px H. simpls. split~. apply~ Cont. intros j y1 y2 Ryx. apply~ (H (y1,y2)). subst f. intros x1 x2. apply~ (H1 (x1,x2)). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)