improvements to unifyLib

- parameterise the conversions on the subterm evaluator rather than using EVAL
  (add_unify_compset will use CBV_CONV on the provided compset)
- don't insert unnecessary wfs theorems into the database
- expose some basic read/reset functions on the database of wfs theorems
- expose the individual conversions