cases' l₂ with b l₂
case cons.succ
α : 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 α
hl : a :: l₀ <+ l₂
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
h₂ : n✝ + 1 ≤ l₂.length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n✝ + 1
case cons.succ.nil
α : 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
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
hl : a :: l₀ <+ []
h₂ : n✝ + 1 ≤ [].length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ [] ∧ l₁.length = n✝ + 1

case cons.succ.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
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
b : α
l₂ : List α
hl : a :: l₀ <+ b :: l₂
h₂ : n✝ + 1 ≤ (b :: l₂).length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ b :: l₂ ∧ l₁.length = n✝ + 1