Clearly I didn't do as good a job as I'd hoped on making this
directory robust. Changes here are induced by my change to the
choice of names generated for induction theorems involving the string
"type".

Predictably, the same sort of INCLUDE = line is required to get
HolCheck to build.