More precise error message on missing hypothesis
Currently, when I say e.g. iSplit "H1 H2 H3 H4"
and one of the hypotheses does not exist, the error is hypotheses ["H1"; "H2"; "H3"; "H4"] not found in the context.
. This is confusing because it indicates that none of them was found (while actually, only some of them have not been found). It is also not as useful as the error would be if it would name which hypothesis has not been found.
I assume spec patterns have the same issue.