induction' l₀ with a l₀ ih generalizing n l₂
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l₀ <+ l₂
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
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

case cons
α : Type u_1
l l' l₁ : List α
a✝ b : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
l₂ : List α
n : ℕ
hl : a :: l₀ <+ l₂
h₀ : (a :: l₀).length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n