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