induction xs generalizing ys
α : Type
inst✝ : DecidableEq α
xs ys : List α
h1 : xs.length = ys.length
h2 : xs.Nodup
h3 : ys.Nodup
⊢ ∃ f, InjOn f xs ∧ map f xs = ys
case nil
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
⊢ ∃ f, InjOn f [] ∧ map f [] = ys

case cons
α : Type
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (ys : List α), tail✝.length = ys.length → tail✝.Nodup → ys.Nodup → ∃ f, InjOn f tail✝ ∧ map f tail✝ = ys
ys : List α
h1 : (head✝ :: tail✝).length = ys.length
h2 : (head✝ :: tail✝).Nodup
h3 : ys.Nodup
⊢ ∃ f, InjOn f (head✝ :: tail✝) ∧ map f (head✝ :: tail✝) = ys