У меня есть следующая цель Изабель:

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

Ни одна из тактикsimp, fast, clarsimp, blast, fastforceи т.д. добиться прогресса в достижении цели, несмотря на то, что она довольно проста.

Почему Изабель просто не упрощает телоif построить так, чтобы оба «a ≠ a» и «b ≠ b» сталиFalseи, следовательно, решить цель?