proposition: Lemma S_equaz_law1 : Equalizer_law1 f S_equaz_mor.
proof: Proof. unfold Equalizer_law1, Equalizer_eq, S_equaz_mor in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *; unfold Comp_fun in |- *; simpl in |- *; unfold Id_fun in |- *. intros i j x; elim x; simpl in |- *; auto. Qed.
imports: Equalizers Setoid_prop SET