experiment with automatising termination argument

lem now has the ability to use Define instead of Hol_defn. This should
make most of our termination theories shrink substantially.