`wp_rec` splits the goal via `wp_bind` where Rocq keeps it flat

[kdvkrs]

Surfaced while working on wp_apply. Related to #480.

wp_rec reduces the redex under a wp_bind, so the surrounding evaluation context ends up
in the postcondition instead of staying in the WP expression:

-- (l ↦ some v) ⊢ WP hl((#(); !v(#l)) + #1) @ s ; E {{ _r, True }}
  wp_seq
-- Lean: ⊢ WP hl(!#l) {{ v, WP hl((v(&v) + #1)) {{ _r, True }} }}
-- Rocq:   WP ! #l + #1 {{ _, True }}

Visible whenever the evaluation context is non-empty and the body does not reduce to a value. Downstream
goals then differ from Rocq's.

Cause. Iris/Iris/HeapLang/ProofMode.lean:378

macro "wp_rec" : tactic =>
  `(tactic | (wp_bind _ _; iapply $(mkIdent `wp_rec):ident; rfl; imodintro; wp_finish))

Rocq's wp_rec does two things: (a) it takes the beta step in context, leaving one flat WP,
and (b) it unfolds the head constant to a rec-value, which wp_pure/wp_pures deliberately
never do (so wp_pures terminates on recursive functions). (Rocq's AsRecV_recv assert is
Ltac plumbing for (b).) The current implementation gets (b) right, since iapply/rfl work up to
defeq, but loses (a): nothing puts K back. Routing wp_rec through
wp_pure (App _ _) like Rocq would invert the trade: tac_wp_pure restores K, but instance
synthesis will not unfold a def to a RecV.

Affects wp_rec, wp_lam, wp_let, wp_seq, wp_match, and the try wp_seq
fast-forward in wp_store/wp_xchg from #600.

Happy to fix this myself.