simp only [List.InjOn]
case left
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ InjOn id []
case left
α : Type
inst✝ : DecidableEq α
ys : List α
h1 : [].length = ys.length
h2 : [].Nodup
h3 : ys.Nodup
s1 : ys = []
⊢ ∀ ⦃x₁ : α⦄, x₁ ∈ [] → ∀ ⦃x₂ : α⦄, x₂ ∈ [] → id x₁ = id x₂ → x₁ = x₂