Hello,
Right now, the syntax for a scheme looks like:
```
Scheme-Block = "scheme" Scheme-Identifier "{" Scheme-Parameters "}" ":"
Scheme-Conclusion [ "provided" Scheme-Premise { "and" Scheme-Premise } ]
( "proof" | ";" )
Reasoning "end" .
```
I am proposing we change the `( "proof" | ";" )` to just `"proof"`, i.e.,
```
Scheme-Block = "scheme" Scheme-Identifier "{" Scheme-Parameters "}" ":"
Scheme-Conclusion [ "provided" Scheme-Premise { "and" Scheme-Premise } ]
"proof"
Reasoning "end" .
```
...or even better...
```
Scheme-Block = "scheme" Scheme-Identifier "{" Scheme-Parameters "}" ":"
Scheme-Conclusion [ "provided" Scheme-Premise { "and" Scheme-Premise } ]
Proof .
```
This change adheres to the principle of least surprise: theorems require either a justification or a `Proof` as a justification, schemes should have a similar structure (but only `Proof` makes sense, really).
Only two schemes currently do not adhere to this proposed syntax (one in FIELD_16, another in PRE_CIRC).
And the change requires only minimal changes to the parser.
Best,
Alex