Proof judgement ADT, sugars and printer

Created by: FlorianCassayre

Proof judgement

sealed abstract class SCProofCheckerJudgement:
  def isValid: Boolean

case object SCValidProof extends SCProofCheckerJudgement
case class SCInvalidProof(path: Seq[Int], message: String) extends SCProofCheckerJudgement

Structurally equivalent to an Option[(Seq[Int], String)], but makes more sense.

Incorrect indentation in Printer

The negative indices weren't aligned with the rest (this was introduced by a careless copy paste).

Missing syntactic sugars

Added the following missing syntactic sugars:

• Pattern matching extractors for infix/unary operators

  formula match
    case a ==> b => ...
    case a <=> b => ...

• Sequent from tuples and various other collections

  () |- (a, b)

• Conversions of terms to labels