Add cartesian products to all concrete set types

This adds a set Cartesian product on:

• list
• gset
• propset
• boolset
• listset

With the notation A × B at level 37. The notation is left associative so that lA × lB × lC : list (A * B * C). This includes corresponding specification lemmas and SetUnfoldElemOf instances. I only did a set level specification. There is no lemma in this MR describing the order for the Cartesian product on lists (the only one of those types where order is relevant)