exact (exists_sublist_length_eq h₂).imp (fun l₁ h ↦ ⟨nil_sublist _, h⟩)
case nil
α : Type u_1
l l' l₁ : List α
a b : α
m : ℕ
l₂ : List α
n : ℕ
hl : [] <+ l₂
h₀ : [].length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, [] <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
no goals