proposition: Lemma S_together_r : Map2_congr_law S_together.
proof: Proof. unfold Map2_congr_law in |- *; simpl in |- *; intros f f' g H; unfold Ext in |- *; simpl in |- *. intro c; unfold Equal_Sprod in |- *; simpl in |- *; split. apply (H c). apply Refl. Qed.
imports: SetoidPROD Binary_Products SET