Add logic for parsing user guides

[ZachJHansen]

A user guide should not contain any annotated formulas other than

role: assumption
direction: universal

Otherwise an error should be thrown.

If any function constants other than placeholders occur in the formulas of a user guide, specification, or proof outline, a warning should be issued.

[ZachJHansen]

Furthermore, lemmas are out of place in the specification. Specifications should include assumptions and specs only. Assumptions and specs marked with directions other than universal should include a "do you know what you're doing?" warning.