wp_apply first performs
wp_pures, which might cause the goal to be normalized too far.
We experienced this issue in Actris, see https://gitlab.mpi-sws.org/iris/actris/-/blob/master/theories/examples/basics.v#L358, where we had to carefully call
wp_pure for a certain number of times, and then
iApply the lemma.
This MR fixes this issue by letting adding a new variant
wp_smart_apply that performs
wp_pure step-by-step. The old
wp_apply now performs no reduction whatsoever.