proposition: Lemma S_pulb_law2 : Pullback_law2 S_pulb_p S_pulb_diese.
proof: Proof. unfold Pullback_law2, Pullback_eq2 in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *; intros; simpl in |- *. apply Refl. Qed.
imports: Pullbacks Setoid_prop SET SetoidPROD