possible route for proving wfs during EVAL

keeps a database of substitutions known to be wfs and updates it after
every call to unify. uses the database to discharge the wfs
side-condition for unify, vwalk, and oc.