proposition: Lemma Mor_prod_r : Map2_congr_law Mor_prod.
proof: Proof. unfold Map2_congr_law in |- *; intros f f' g H. unfold Mor_prod in |- *. apply (Prf_map2_congr (Op_together (C1 c d) _) (a1:=Proj1_prod (C1 a b) o f) (a2:=Proj1_prod (C1 a b) o f') (Proj2_prod (C1 a b) o g)). apply Comp_l. trivial. Qed.
imports: Category Map2