induction l generalizing l₁ with
| nil => exact l₁.length.zero_le
| cons a l IH =>
  have .cons nodup_head (nodup_tail : l.Nodup) := nodup
  let ⟨ha,hl⟩ := cons_subset.mp h
  clear nodup h
  have ⟨l₁', l₁'', hl₁⟩ := mem_iff_append.mp ha
  cases hl₁; clear ha
  have : l ⊆ l₁' ++ l₁'' := fun b hb => 
    match mem_append.mp (hl hb) with
    | .inl hb => mem_append.mpr <| Or.inl hb
    | .inr hb => mem_append.mpr <| Or.inr <|
      match hb with
      | .head _ => absurd rfl <| nodup_head b ‹b ∈ l›
      | .tail _ h => h
  specialize IH nodup_tail this
  simp only [length_append, length_cons] at IH ⊢
  exact Nat.succ_le_succ IH
α : Type u
β : Type v
l l₁ : List α
nodup : Nodup l
h : l ⊆ l₁
⊢ length l ≤ length l₁
no goals