| Statement (f, n, t, v, s) -> mk_statement f n t v :: mk_thnote s a
| Inductive (lps, ts, s) -> mk_inductive lps ts :: mk_thnote s a
| Qed s -> mk_qed :: mk_tacnote s a
| Statement (f, n, t, v, s) -> mk_statement f n t v :: mk_thnote s a
| Inductive (lps, ts, s) -> mk_inductive lps ts :: mk_thnote s a
| Qed s -> mk_qed :: mk_tacnote s a