| Id s -> mk_note s :: cont sep (mk_id :: a)
| Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
| Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a)
| Id s -> mk_note s :: cont sep (mk_id :: a)
| Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
| Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a)