simpa using h₂
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.176184 → Type ?u.176186
α : Type u_1
β : Type ?u.176192
inst✝¹ : Monad m
inst✝ : DecidableEq α
b a : α
l : List α
h₁ : b ∈ l
h₂ : ¬b = a
⊢ (!decide (b = a)) = true
no goals