Attempt to clear a goal obtained by refining a pi_instance goal.

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.

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.