Ordinals and (Half of) Transfinite Recursion

Adding more set theory stuff. Developing ordinals and hoping to have transfinite recursion soon!

Dedicated to the two great banes of my existence:

val firstInPairReduction = Lemma(
    () |- (firstInPair(pair(x, y)) === x)
  )
val secondInPairReduction = Lemma(
    () |- (secondInPair(pair(x, y)) === y)
  )

Other technical changes:

• subproof now checks the provided statement for correctness and introduces a Restate step if necessary to present itself correctly.
• introduced a lastStep helper, which can be used to refer to the, guess what, last step. Intended use case is when steps are named just because the step following them is a two-premise tactic. This is a fairly common pattern. Example:

val prem = have( A |- B ) by Magic // generic step to be used multiple times or mark a point in the proof
// ... things happen
val step2 = thenHave( B |- D ) by Magic // minor step that only has to be used once
have( A |- C ) by Cut(prem, step2)

// the above changes to 
val prem = have( A |- B ) by Magic // generic step to be used multiple times or mark a point in the proof 
// ... things happen
thenHave( B |- D ) by Magic // minor step that only has to be used once
have( A |- C ) by Cut(prem, lastStep)

• added some OL kernel helpers. Two of these are required to fix alpha equivalence in Cut parameter inference, the rest have been added for completeness.
  • +<? add a formula to the left of a sequent if an OL equivalent does not exist
  • +>? add a formula to the right of a sequent if an OL equivalent does not exist
  • ++<? add the LHS of a sequent to an existing sequent, dropping formulas for which OL equivalents exist
  • ++>? add the RHS of a sequent to an existing sequent, dropping formulas for which OL equivalents exist
  • ++? add the LHS and RHS of a sequent to an existing sequent, dropping formulas for which OL equivalents exist
• Fixed param inference in Cut to allow alpha-eq formulas; and more generally, now, OL eq.