Improving `ipose`

[lzy0505]

TODO: Needs clean up

This PR improves ipose in the following ways:

1. Support posing arbitrary terms (e.g. global theorems), not just local hypotheses, via elabTerm.

2. Following Rocq, unified IntoEmpValid via a single intoEmpValid_here instance that delegates to AsEmpValid2.

3. Use whnf reduction to expose foralls and implications hidden behind let-bindings.

4. Following Rocq, added EmpValid to handle emp ⊢ P case.

5. Added some docstrings.

6. Moved existing ipose tests and added more cases in src/Iris/Tests/Tactics/Pose.lean.