added a '(x == y = True) -> (x = y)' lemma