cases h3
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h3 : ys_hd ∉ ys_tl ∧ ys_tl.Nodup
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl
case intro
α : Type
inst✝ : DecidableEq α
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List α), xs_tl.length = ys.length → xs_tl.Nodup → ys.Nodup → ∃ f, InjOn f xs_tl ∧ map f xs_tl = ys
ys_hd : α
ys_tl : List α
h1 : xs_tl.length = ys_tl.length
h2_left : xs_hd ∉ xs_tl
h2_right : xs_tl.Nodup
left✝ : ys_hd ∉ ys_tl
right✝ : ys_tl.Nodup
⊢ ∃ f, InjOn f (xs_hd :: xs_tl) ∧ map f (xs_hd :: xs_tl) = ys_hd :: ys_tl