Theorem: FreeGroup.nil_nextVertex (GroupComp/WordProblem/FreeGroup.lean)

State before:
α : Type
inst✝ : DecidableEq α
letter : α × Bool
⊢ [] :+ letter = [letter]
Tactic:
rfl
State after:
no goals