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

State before:
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
red : Reduced start
⊢ finalVertex start word = finalVertexOnFreeGroup start red (mk word)
Tactic:
rfl
State after:
no goals