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