Elaborate e as an application whose last argument is a do← body, performing the effect
forwarding. Returns none if e doesn't have that shape.
Strategy: build headApp ?forwarded with a fresh metavariable in the body slot and elaborate
it. Lean's elaborator handles named args, defaults, and dot notation. We then check the
wrapper's shape against the probe; on success, the lifted body is assigned into ?forwarded
and the probe expression itself is the result.