proposition: Lemma Mor_prod_l : Map2_congl_law Mor_prod.
proof: Proof. unfold Map2_congl_law in |- *; intros f g g' H. unfold Mor_prod in |- *. apply (Prf_map2_congl (Op_together (C1 c d) _) (b1:=Proj2_prod (C1 a b) o f) (b2:=Proj2_prod (C1 a b) o g) (Proj1_prod (C1 a b) o g')). apply Comp_l. trivial. Qed.
imports: Category Map2