apply Exists.elim xs_ih
α : 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
xs_ih : ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ 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
xs_ih : ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys_tl
⊢ ∀ (a : α → α),
    InjOn a xs_tl ∧ map a xs_tl = ys_tl → ∃ f, InjOn f (xs_hd :: xs_tl) ∧ f xs_hd = ys_hd ∧ map f xs_tl = ys_tl