Added one case with the indirect equality test to check for the (still absent) feature:
    o using previously proved theorems
    o testing the relation between first and last step: all the steps shouldn't be quantified over universally
added the indirect inequality proof tactic