cases
induction
Motivation: improve the effectiveness of the `save` and `checkpoint` tactics.
{}
String.Pos
·
.
simp