case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
a₁✝ : FreeGroup α
L₁ : List (α × Bool)
a₂✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L₁) = toWord (Quot.mk Red.Step L₂) → Quot.mk Red.Step L₁ = Quot.mk Red.Step L₂
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ Function.Injective toWord
rintro ⟨L₁⟩ ⟨L₂⟩
no goals
case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
a₁✝ : FreeGroup α
L₁ : List (α × Bool)
a₂✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L₁) = toWord (Quot.mk Red.Step L₂) → Quot.mk Red.Step L₁ = Quot.mk Red.Step L₂
exact reduce.exact