Theorem: Word.cons_eps (FormalSystems/Preliminaries/Word.lean)

State before:
α✝ : Type u_1
w : α✝
⊢ w :: ε = [w]
Tactic:
simp
State after:
α✝ : Type u_1
w : α✝
⊢ ε = []

State before:
α✝ : Type u_1
w : α✝
⊢ ε = []
Tactic:
rfl
State after:
no goals