Theorem: List.nil_isPrefix (One.lean)

State before:
α✝ : Type u_1
l : List α✝
⊢ [] <+: l
Tactic:
unfold List.isPrefix
State after:
α✝ : Type u_1
l : List α✝
⊢ ∃ t, [] ++ t = l

State before:
α✝ : Type u_1
l : List α✝
⊢ ∃ t, [] ++ t = l
Tactic:
exists l
State after:
no goals