proposition: Lemma Eq1_Sprod : Eq1_prod_law (Proj1_SPROD A B) S_op_together.
proof: Proof. unfold S_op_together, Eq1_prod_law in |- *; simpl in |- *; intros C f g. unfold Ext in |- *; simpl in |- *. intro c; apply Refl. Qed.
imports: SetoidPROD Binary_Products SET