Theorem: List.isInfix_self (One.lean)

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