Consistent handling of pure implication and forall
It required a bunch of additional proof mode type class instances and a hack for iSpecialize
to deal with an inconsistent behavior of refine
.
I hope this covers all cases.
It required a bunch of additional proof mode type class instances and a hack for iSpecialize
to deal with an inconsistent behavior of refine
.
I hope this covers all cases.