fix: wp_rec keeps the evaluation context flat

[kdvkrs]

Description

This PR fully addresses #603 and is comprised of two commits:

• commit 1 changes the definitions of wp_match, wp_seq, and wp_let to use wp_pure (_ _) instead of wp_rec because they do not require unfolding. This fixes the first part of wp_rec splits the goal via wp_bind where Rocq keeps it flat #603 even without redefinition of wp_rec but is still an arguably cleaner path since the unfolding route does not need to be invoked.
• commit 2 extracts the body of wp_pure into a shared core with wp_rec that takes an unfoldHead parameter and redefines wp_rec on top of it. wp_rec thus no longer calls wp_bind and leaves a flat goal like the Rocq counterpart. This fixes the second part of #603

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.

[MackieLoeffel]

Thanks for the PR! I slightly refactored the PR to make iWPPure more generic, but otherwise it looks great!