simp only [length_append, length_cons] at IH ⊢
case cons.refl
α : Type u
β : Type v
a : α
l : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
IH : length l ≤ length (l₁' ++ l₁'')
⊢ length (a :: l) ≤ length (l₁' ++ a :: l₁'')
case cons.refl
α : Type u
β : Type v
a : α
l : List α
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
l₁' l₁'' : List α
hl : l ⊆ l₁' ++ a :: l₁''
this : l ⊆ l₁' ++ l₁''
IH : length l ≤ length l₁' + length l₁''
⊢ Nat.succ (length l) ≤ length l₁' + Nat.succ (length l₁'')