| Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a)
| Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a)
| Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a)
| Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a)
| Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a)
| Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a)