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.