split_ifs
case h
α : Type
inst✝ : DecidableEq α
a x : α
⊢ (if x = a then a else id x) = id x
case pos
α : Type
inst✝ : DecidableEq α
a x : α
h✝ : x = a
⊢ a = id x

case neg
α : Type
inst✝ : DecidableEq α
a x : α
h✝ : ¬x = a
⊢ id x = id x