add a simple coq-subset parser and use it in insert.rkt
so that we can avoid a new notation with code fragments
in the paper