Forbid references to formulas in discharged flags

The following proof should not be accepted, as the assumption p of the flag (and anything proven from it) should be discharged when the flag is closed.

| p
p : copy 1

Exceptions to this are of course rules that introduce hypotheses via flags, like ∃-elimination.

This also leads to Proof Rondo accepting proofs where a subproof should be under the scope of a flag. For instance, the following should not be accepted.

p
p
p -> p : -> i 1-2