proposition: Lemma Unique_S_together : Unique_together_law (Proj1_SPROD A B) (Proj2_SPROD A B) S_op_together.
proof: Proof. unfold Unique_together_law, S_op_together in |- *; simpl in |- *; intros C h. unfold Ext in |- *; simpl in |- *. intro c; unfold Equal_Sprod in |- *; simpl in |- *; split; apply Refl. Qed.
imports: SetoidPROD Binary_Products SET