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