Theorem: BVDecide.SatAtBVLogical.false_of_eq_true_of_eq_false (LeanSAT/Reflect/Tactics/BVDecide.lean)

State before:
x : Bool
h₁ : x = true
h₂ : x = false
⊢ False
Tactic:
cases h₁
State after:
case refl
h₂ : true = false
⊢ False

State before:
case refl
h₂ : true = false
⊢ False
Tactic:
cases h₂
State after:
no goals