Theorem: List.isInfix_append_left (One.lean)

State before:
α : Type u_1
l₁ l₂ : List α
⊢ l₁ <:+: l₁ ++ l₂
Tactic:
exact ⟨ [], l₂, rfl⟩
State after:
no goals