| `Term term2 -> " exact " ^ NotationPp.pp_term status term2
| `Proof -> " proof"
| `SolveWith term -> " using " ^ NotationPp.pp_term status term)
| `Term term2 -> " exact " ^ NotationPp.pp_term status term2
| `Proof -> " proof"
| `SolveWith term -> " using " ^ NotationPp.pp_term status term)