rintro (_ | _)
case mp
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ b :: l₂ → a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂
case mp.cons
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
a✝ : a :: l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂

case mp.cons₂
α : Type u_1
l l' l₀ l₁ l₂ : List α
a : α
m n : ℕ
a✝ : l₁ <+ l₂
⊢ a :: l₁ <+ l₂ ∨ a = a ∧ l₁ <+ l₂