Giving true proof-terms in inversion instead of metas.
Rewriting [lapply] tactic in the new monad.