<p>We already have a pointwise product setoid in the lib; see Relation.Binary.Product.Pointwise.</p>
<p>Gergo</p>