Theorem: List.isInfix_append_right (One.lean)

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