proposition: Lemma S_pulb_map_law : Map_law S_pulb_fun.
proof: Proof. unfold Map_law in |- *; simpl in |- *; unfold Equal_Sprod in |- *; simpl in |- *. intros x y H1; split; apply Pres1; trivial. Qed.
imports: Pullbacks Setoid_prop SET SetoidPROD