This module implements the proof verification algorithm for Fitch-style natural deduction Proofs. Given a map of RuleSpecs, it checks each line by verifying that its RuleApplication is applied correctly.

Phases of proof verification:

1. Check that the rule exists
2. Check that the formula matches the rules' conclusion.
3. Match references to lines/proof, concretely: - check that references are parsed and valid line numbers - line references should only refer to lines - proof references should refer to proofs, i.e. first number is the first line and second number the conclusion - referenced line needs to be visible for the referer, i.e. not in a subproof or later in the proof. - unify referenced lines with expected formula/proof.
4. Collect name->term mappings.
5. Verify name->term mappings, the datastructure should be `Map Name [(Int, Term)]` to give better error messages. The Int is the corresponding line number.
6. Collect name->formula mappings, using the name->term mappings to resolve substitutions. The datastructure for name->formula mappings should be `Map Name [Either RawFormula [RawFormula]]`, where Name is e.g. φ, RawFormula is a formula that has been identified as φ, and `[RawFormula]` is a list of possible formulae that can be identified as φ (yielded by backwards-substitution).
7. Now check that for every φ all its mappings can be made equal by choosing from the lists.

It also provides checkFreshness for validating fresh-variable tAssumptions, and regenerateSymbols for collecting and validating function- and predicate-symbol arities across the whole Proof.