proposition: Lemma prod_cofe : forall I A1 A2 (F1:family I A1) (F2:family I A2), COFE F1 -> COFE F2 -> family_r F1 = family_r F2 -> COFE (prod_family F1 F2).
proof: Proof. Proof using. introv Cofe1 Cofe2 Eqr. apply prod_cofe_sim. destruct F1 as [R1 S1]. auto. destruct F2 as [R2 S2]. rewrite Eqr. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)