Premises from outside of a subproof
In the case of veriT, a step in a subproof can never use the conclusion of a step from outside the subproof. Cvc5, however, can do this. We need to investigate if this is always fine and clarify this in the document.