Fix proof broken by change to drule in 812a08a5a8

Basically, the old behaviour can be recovered by using

FREEZE_THEN drule

instead of just drule.

Fix examples/boyer_moore for tight equality

Removed trailing whitespace

Added Boyer Moore substring search algorithm implementation (on lists and strings) to examples