α : Type u_1
l₁ l₂ l₃ : List α
⊢ l₂ <:+: l₁ ++ l₂ ++ l₃
α : Type u_1
l₁ l₂ l₃ : List α
⊢ l₂ <:+: l₁ ++ (l₂ ++ l₃)
rw [← List.append_assoc]
no goals
α : Type u_1
l₁ l₂ l₃ : List α
⊢ l₂ <:+: l₁ ++ l₂ ++ l₃
apply infix_append