proposition: Lemma FixValModMut2_fix : 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) (x1:A1) (x2:A2), (x1,x2) = FixValModMut2 E1 E2 F1 F2 -> prod2 E1 E2 = similar M -> COFE M -> valmut2_contractive_noinv M F1 F2 -> E1 x1 (F1 x1 x2) /\ E2 x2 (F2 x1 x2).
proof: Proof. Proof using. introv Defx SimE Cofe Contr. forwards~ (H1&H2&_): (@FixValModMut2_fix_inv I A1 A2 _ _ M E1 E2 F1 F2 (fun _ _ _ => True) x1 x2). intros_all. forwards~ Z: Contr. intros. forwards*: H. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)