Searchxxx now interpret patterns in goal environment if any.

This makes such things work:

x:nat
h: x = 3
================
True

Search x.