Get rid of locked value lambdas

I noticed that various people (including yours truly) often get confused by the fact the parsing of (λ: x, e)%V adds a locked, while both LamV x e and locked (LamV x e) are pretty printed as λ: x, e. As a result of these sneaky occurrences of locked, it is often the case that lemmas or hypotheses that appear to be the same do not actually match. This MR repairs this situation by getting rid of locked.

The main point of the locked trick was to avoid wp_pures to unfold lambdas/recs that are hidden behind a definition. E.g., wp_pures should not unfold foo v with:

Definition foo := λ: "x", ...

In this MR I propose another approach:

• Use a Hint Extern to detect lambdas/recs. This will only work if they are not hidden behind a definition.
• For wp_rec/wp_lam add an instance that recognizes lambdas/recs even if they are behind a definition.

Consequences:

• As a result of this MR I was able to remove some hacks, i.e. we no longer need to write LamV ... in the %V notations for e.g. par; we can now just use the λ: notation there.
• Iris-examples compile without any changes.