proposition: Lemma FixValModMut2_fix_inv : forall (I A1 A2:Type) {IA1:Inhab A1} {IA2:Inhab A2} (M:family I (A1*A2)) (E1:binary A1) (E2:binary A2) (F1:A1->A2->A1) (F2:A1->A2->A2) (Q:I->A1->A2->Prop) (x1:A1) (x2:A2), (x1,x2) = FixValModMut2 E1 E2 F1 F2 -> prod2 E1 E2 = similar M -> COFE M -> valmut2_continuous M Q -> valmut2_contractive M F1 F2 Q -> E1 x1 (F1 x1 x2) /\ E2 x2 (F2 x1 x2) /\ forall i, (Q i x1 x2).
proof: Proof. Proof using. introv Defx SimE Cofe Conti Contr. forwards~ [H1 H2]: (@FixValMod_fix_inv I (A1*A2) _ M (prod2 E1 E2) (mutualize2 F1 F2) (fun i p => let (a1,a2) := p in Q i a1 a2) (x1,x2)). intros K u [l1 l2] L uQ i Ki. applys~ Conti. clears x1 x2. intros i [x1 x2] [y1 y2] H. simple~. inversion~ H1. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)