proposition: Lemma S_equaz_reg : Reg_law S_equaz_pred.
proof: Proof. unfold Reg_law, S_equaz_pred in |- *; intros x y H1 H2 i j. apply Trans with (f i x). apply Pres1; apply Sym; assumption. apply Trans with (f j x). apply H2. apply Pres1; assumption. Qed.
imports: Equalizers Setoid_prop SET