apply Quot.ind (β := fun g ↦ mk (reducedWord g) = g )
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
⊢ mk (reducedWord g) = g
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
⊢ ∀ (a : List (α × Bool)), mk (reducedWord (Quot.mk Step a)) = Quot.mk Step a