Late definition usubst clash checking leads to less direct error messages

[rbohrer]

Version: 4.9.8
Reproduce: Upload attached model, then start proof, then run this tactic by hand:
implyR(1); loop("1=1", 1)

Note that running the tactic from a .kyx "Tactic" block does not reproduce the bug, as KeYmaera X inserts an expandAllDefs call

Behavior got: error message just says "repeattactic failed on repetition 1"
Expected: Error message says variable x clashes in definition of "f". Preferably when uploading model.

Possible explanation: In "loop" there is probably a RepeatTactic that expands all necessary definitions automatically. The problem is that if the definition clashes, then expanding it will fail, but the useful part of the error message gets discarded

Priority: More of a quality-of-user-experience thing for project time. Easy to troubleshoot on my end.
late-usubst-error.kyx.txt