proposition: Lemma Comp_Pmor_congl : Congl_law Comp_Pmor.
proof: Proof. unfold Congl_law in |- *; simpl in |- *. unfold Equal_Pmor, Comp_Pmor in |- *; simpl in |- *. intros a b c f g h H. elim H; intros H1 H2; split; apply Comp_l; assumption. Qed.
imports: Category SetoidPROD