Provide an optional comment box along with rules

[NicMcPhee]

At the moment all we allow is the rule (two expressions and their relationship). There are times when, for readability, the writer might wish to include some additional information, e.g.,

• A substitution that helps the reader understand how the rule is being used
• Something like "twice" to indicate that a rule is being multiple times
• Something like "backwards" to indicate that a rule is being used in what might be the "opposite" way of how we typically use it (although that kind of usage probably isn't supported at the moment by the checker)
• Any other comment that might help, like "as proved in the preceding lemma"

This would definitely affect the Markdown output if/when we implement #69.