| 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)
| Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: 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)
| Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: a)