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