-
Use `NoBackTrack` type class for framing with ▷ 1 of 1 checklist item completed!112
-
Generic `iAlways` tactic. 3 of 3 checklist items completed!111 gen_proofmode
-
Weakest preconditions for total program correctness 5 of 5 checklist items completed!65