Theorem: List.isPrefix_self_append (One.lean)

State before:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁ <+: l₁ ++ l₂
Tactic:
exists l₂
State after:
no goals