proposition: Lemma prod_cofe_sim : forall I A1 A2 (R:binary I) (Sim1:I->binary A1) (Sim2:I->binary A2), COFE (Build_family R Sim1) -> COFE (Build_family R Sim2) -> COFE (prod_family_sim R Sim1 Sim2).
proof: Proof. Proof using. introv [[W1 T1 E1] C1] [[W2 T2 E2] C2]; simpls. constructor. constructor; simple~. intros. apply* prod2_equiv. intros K w Down Cohu. unfolds in Cohu. simpls. unfold prod2 in Cohu. forwards~ [l1 L1]: (C1 K (fun i => fst (w i))). intros_all. simpl. specializes Cohu i j. destruct (w j). destruct (w i). apply* Cohu. forwards~ [l2 L2]: (C2 K (fun i => snd (w i))). intros_all. simpl. specializes Cohu i j. destruct (w j). destruct (w i). apply* Cohu. exists (l1,l2). intros_all. unfolds limit. simpls. unfold prod2. specializes L1 i. specializes L2 i. destruct* (w i). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)