The two lines I removed technically assert the exact same thing, since `!a -> b` is equivalent to `a || b`. So, I replaced the two lines with the more symmetric form to make it clearer.