do not make use of wp_bind_inv unnecessarily
@janno asked for this when porting iGPS to PureExec. iGPS does not currently have wp_bind_inv, and it is not clear whether we can make that law hold.
The new ltac in wp_pure
is horrible, I hope @robbertkrebbers can find a better way. :) Ideally, we can make use of the fact that pure_exec_ctx
is an instance. If not, it should probably be downgraded to a lemma.