proposition: Lemma S_equaz_law2 : Equalizer_law2 S_equaz_mor S_equaz_diese.
proof: Proof. unfold Equalizer_law2 in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *; unfold Id_fun in |- *. intros r h p x; apply Refl. Qed.
imports: Equalizers Setoid_prop SET