Ordinals and (Half of) Transfinite Recursion

[sankalpgambhir]

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. 

[sankalpgambhir]

The recursion theorem is getting there, but not quite done. However, the changes and theory development restricted to this branch may be holding up other stuff, so I've documented what is already there, and we can merge this.