Why won't Isabelle simplify the body of my "if _ then _ else" construct?

I have the following Isabelle goal:

lemma "⟦ if foo then a ≠ a else b ≠ b ⟧ ⟹ False"

None of the tactics simp, fast, clarsimp, blast, fastforce, etc. make any progress on the goal, despite it being quite simple.

Why doesn't Isabelle just simplify the body of the if construct so that both "a ≠ a" and "b ≠ b" become False, and hence solve the goal?