proposition: Lemma Comp_dual_congr : Congr_law Comp_Darrow.
proof: Proof. unfold Congr_law in |- *; simpl in |- *. unfold Comp_Darrow in |- *; simpl in |- *. intros a b c f g h eqf_g. unfold DHom in |- *; apply Comp_l; apply eqf_g. Qed.
imports: Category