constructor
α : 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
α : 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 mpr
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
⊢ a :: l₁ <+ l₂ ∨ a = b ∧ l₁ <+ l₂ → a :: l₁ <+ b :: l₂