Proof checking at the level of tactics

Replicating proof checking at the level of construction of DoubleStep based proofs. Supersedes #93 following changes in #99.

• [implementation] the checks for fully parametrized versions of steps replicate checks from SCProofChecker
  • Except in the case of SUBPROOF, which implements its own exception-based checking.
• [implementation] where possible, unparameterized versions defer checking by calling the parametrized versions, to centralize checking for a given proof step
• [documentation] error messages have been uniformized in tone and speech patterns where spotted. I have opted for active instead of passive tones wherever applicable, "x is not y" instead of "x must be y". Previously, both existed simultaneously.
• [bug] problems with overload resolution (#100) by removing overloaded instances of apply within proof tactics, which are instead replaced with apply for the parameterles versions, and (...).withParameters() for the explicit version where necessary.

Status:

• ✔ Left propositional rules
• ✔ Right propositional rules
• ✔ Reflexivity rules
• ✔ Substitution rules
• ✔ Instantiation rules
• ✔ Printing abstracted proofs with errors (#85) (Solved with #99)