Make `iAssumption` work on `⊢ ...` premises in the Coq context.
Moreover, fix errors of iAssumption, iExact, and friends.
- The error messages were wrong: the goal needs to be absorbing, not the hypothesis.
- The wrong failure number was used in
iAssumption, which caused the error not to be propagated properly.