split_ifs
case h
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
⊢ (if x = a then c else if x = a then b else f x) = if x = a then c else f x
case pos
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
h✝ : x = a
⊢ c = c

case neg
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b c : β
x : α
h✝ : ¬x = a
⊢ f x = f x