| LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a
| Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a
| Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a
| LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a
| Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a
| Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a