Transfinite Recursion (part 2) (!156) · Merge requests · LARA / lisa

Sankalp Gambhir requested to merge github/fork/sankalpgambhir/transfinite-contd into main Apr 20, 2023

This time, it's back for revenge.

What we have: ✔ Well Ordered Induction 〰 Well Ordered Recursion ✔ Transfinite Induction (couple of missing tiny baby little lemmas using sorry) :crossed_fingers: Transfinite Recursion

Any fixes or changes: 👍 Relies on #159 and #160 locally, please don't merge yet <- these were merged :) ⚙ Fix UniqueComprehension breaking due to assumptions after #160 .

Transfinite Recursion (part 2)

Merge request reports