proposition: Lemma Together1_l : Map2_congl_law Together1.
proof: Proof. unfold Map2_congl_law in |- *; intros f g g' H'. unfold Together1 in |- *. apply (Codiese_map ua' (a':=c)). simpl in |- *; unfold Equal_Pmor in |- *; simpl in |- *. split. apply Refl. trivial. Qed.
imports: Diagonal CCC Terminal1