apply Exists.intro id
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ ∃ f, InjOn f [] ∧ map f [] = []
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ InjOn id [] ∧ map id [] = []