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

State before:
α : Type
inst✝ : DecidableEq α
⊢ Reduced []
Tactic:
apply not_step_nil
State after:
no goals