proposition: Lemma S_equaz_law3 : Equalizer_law3 S_equaz_mor S_equaz_diese.
proof: Proof. unfold Equalizer_law3 in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *; unfold Equal_SubType in |- *; simpl in |- *. unfold Id_fun, S_equaz_ob in |- *; intros r h p l H x. apply Sym; apply H. Qed.
imports: Equalizers Setoid_prop SET