Use `notypeclasses refine` in `iPoseProof` helpers.
Also, rewrite `iIntoEmpValid`. Now, instead of using Ltac to traverse the type of the term and generate goals for the premises, we repeatedly apply a series of lemmas. This has the advantage that it works up to convertability, and we no longer need the `eval ...` hacks.
Showing with 48 additions and 69 deletions