Theorem: List.nil_isInfix (One.lean)

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

State before:
α✝ : Type u_1
l : List α✝
⊢ ∃ s t, s ++ [] ++ t = l
Tactic:
exists []
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