intro h
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
⊢ ¬a = b → (f a && decide (a = b)) = (f b && decide (a = b))
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
h : ¬a = b
⊢ (f a && decide (a = b)) = (f b && decide (a = b))