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

State before:
α : Type
inst✝ : DecidableEq α
p : α × Bool
⊢ Reduced [p]
Tactic:
intro L' step
State after:
α : Type
inst✝ : DecidableEq α
p : α × Bool
L' : List (α × Bool)
step : Step [p] L'
⊢ False

State before:
α : Type
inst✝ : DecidableEq α
p : α × Bool
L' : List (α × Bool)
step : Step [p] L'
⊢ False
Tactic:
apply not_step_singleton step
State after:
no goals