Automation for creating instances of mathematical structures for pi types
pi_instance constructs an instance of
my_class (Π i : I, f i)
where we know
Π i, my_class (f i). If an order relation is required,
it defaults to
pi.partial_order. Any field of the instance that
pi_instance cannot construct is left untouched and generated as a new goal.