| Tactic is run (ideally only once) | |
| Tactic is run (ideally only twice) | |
| Tactic is run (ideally only twice) | |
| Tactic is run (ideally only once, in most general context) | |
| n : Nat | |
| ⊢ n < n.succ | |
| Tactic is run (ideally only twice, in most general context) | |
| Tactic is run (ideally only twice, in most general context) | |
| n : Nat | |
| ⊢ n < n.succ | |
| n m : Nat | |
| ⊢ n < n.succ |