search works incorrectly for false assumptions

[chaudhuri]

This does not appear to work but should.

Kind i type.
Type a,b i.

Theorem fails : a = b -> b = a.
search.

This was brought to my attention by @robblanco.