Proof checking at higher abstraction level

Replicating proof checking at the level of construction of DoubleStep based proofs.

• the checks for fully parametrized versions of steps replicate checks from SCProofChecker
• where possible, unparameterized versions defer checking by calling the parametrized versions, to centralize checking for a given proof step
• 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.
• a requirement during checking was to make sure the correct number of premises has been provided to the step. A suggestion offered was to make the step a function of arity N where N is a type parameter provided as ProofStepWithoutBotNorPrem[N]. I have not found a way to do this in Scala yet, outside of adding a require statement to the function, which in my opinion, produces a relatively unhelpful error message with respect to tracking it down. Currently, I have implemented them as part of the proof checking, and an error is raised in the same manner as a malformed proof step:

if (premises.length != 2)
        invalid(s"Two premises expected, ${premises.length} received.")

Status:

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

However, in the short term, this will make error reporting worse till #85 is resolved, since all the errors are expected to be reported through the tactic system. DO NOT MERGE before it is resolved or the status is accordingly updated above.