make wp_apply not call wp_pures

Currently, wp_apply calls wp_pures before trying to apply the lemma, which can be a problem when the user needs more control over the shape of the goal to actually make the lemma apply. I ran into this with wp_expr_eval simpl simplifying things too far; @robbertkrebbers said he had similar problems with wp_pures reducing too far (for lemmas whose conclusion still contain redexes).

This MR just removes that call. However, that had more fallout than I expected, so I wonder if we should instead have two tactics -- one with and one without the implicit simplification.