Now applies theorems which are self-binding

Example: (|S| = 0) = (S = Empty_String)
Previously this would be ignored since it does not require a search.
Now any theorem which does not produce a match conjunction will attempt
to produce bindings from its own registry.