proposition: Lemma S_pulb_reg : Reg_law S_pulb_pred.
proof: Proof. unfold Reg_law, S_pulb_pred in |- *; intros a1xc1 a2xc2 H1 H2. elim H1; intros H3 H4. apply Trans with (f (Sprod_l a1xc1)). apply Pres1; apply Sym; assumption. apply Trans with (g (Sprod_r a1xc1)). assumption. apply Pres1; assumption. Qed.
imports: Pullbacks Setoid_prop SET SetoidPROD