split_ifs
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
⊢ (if x = xs_hd then f ys_hd else updateListITE f xs_tl (List.map f ys_tl) x) =
    if x = xs_hd then f ys_hd else updateListITE g xs_tl (List.map f ys_tl) x
case pos
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
h✝ : x = xs_hd
⊢ f ys_hd = f ys_hd

case neg
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), updateListITE f xs_tl (List.map f ys) x = updateListITE g xs_tl (List.map f ys) x
ys_hd : α
ys_tl : List α
h✝ : ¬x = xs_hd
⊢ updateListITE f xs_tl (List.map f ys_tl) x = updateListITE g xs_tl (List.map f ys_tl) x