proposition: Lemma Comp_Pmor_congr : Congr_law Comp_Pmor.
proof: Proof. unfold Congr_law in |- *; simpl in |- *. unfold Equal_Pmor, Comp_Pmor in |- *; simpl in |- *. intros a b c f g. elim f; elim g; simpl in |- *. intros gl gr fl fr H h. elim h; simpl in |- *. intros hl hr. elim H; intros H1 H2; split; apply Comp_r; assumption. Qed.
imports: Category SetoidPROD