Errors

Created by: SimonGuilloud

Redone most of the tactics system. Some things that were checked at runtime are now checked at compile time. Type structure should be clearer and simpler. Writing tactics should be as simple as:

object MyTactic extends ProofTactic {
    def apply(using proof: Library#Proof)(arbitrary args)(premise: proof.Fact)(bot: Sequent): proof.ProofTacticJudgement =
        ???
}

There is now an actual error report system, printing the higher level proofs, showing faulty line and proof tactic. Subproofs are fully suported.

ProofSteps are now ProofTactics DoubleSteps are now ProofSteps