We only use wp_value in the end if the resulting goal is yet
another wp. Otherwise we may not be able to do a final view
shift (as observed by Ralf).

It now also reshapes expressions as values for contexts that need
values such as AppECtx.

Turns out it only holds as a view shift, not as an implication

I thought I could derive an interesting Lemma from this. Turns out I cannot. But this one may still be useful, at some point.