proposition: Lemma S_pulb_law1 : Pullback_law1 f g S_pulb_p S_pulb_q.
proof: Proof. unfold Pullback_law1, Pullback_eq1 in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *; intro x; elim x; unfold Comp_fun in |- *; simpl in |- *. trivial. Qed.
imports: Pullbacks Setoid_prop SET SetoidPROD