On Fri, Jan 11, 2013 at 07:01:41AM +0800, Dr. ??RDI Gerg?? wrote: > We already have a pointwise product setoid in the lib; see > Relation.Binary.Product.Pointwise. > > Gergo This looks good. Thank you. ------ Sergei