apply Exists.intro (Function.updateITE f xs_hd ys_hd)
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ ∃ f,
    (∀ ⦃x₁ : α⦄, x₁ ∈ xs_hd :: xs_tl → ∀ ⦃x₂ : α⦄, x₂ ∈ xs_hd :: xs_tl → f x₁ = f x₂ → x₁ = x₂) ∧
      f xs_hd = ys_hd ∧ map f xs_tl = ys_tl
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
h3_left : ys_hd ∉ ys_tl
h3_right : ys_tl.Nodup
f : α → α
a1_left : InjOn f xs_tl
a1_right : map f xs_tl = ys_tl
⊢ (∀ ⦃x₁ : α⦄,
      x₁ ∈ xs_hd :: xs_tl →
        ∀ ⦃x₂ : α⦄,
          x₂ ∈ xs_hd :: xs_tl → Function.updateITE f xs_hd ys_hd x₁ = Function.updateITE f xs_hd ys_hd x₂ → x₁ = x₂) ∧
    Function.updateITE f xs_hd ys_hd xs_hd = ys_hd ∧ map (Function.updateITE f xs_hd ys_hd) xs_tl = ys_tl