-
Use `NoBackTrack` type class for framing with ▷ 1 of 1 checklist item completed!112
-
Stronger `iNext` that performs arithmetic cancelation 3 of 3 checklist items completed!109
-
Super `iModIntro` tactic that generalizes `iAlways`, `iNext`, `iModIntro`, and more 7 of 7 checklist items completed!121 gen_proofmode