case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f✝ : α → β
x✝ y : FreeGroup α
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
L : List (α × Bool)
⊢ ↑(map g) (↑(map f) (Quot.mk Red.Step L)) = ↑(map (g ∘ f)) (Quot.mk Red.Step L)
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f✝ : α → β
x✝ y : FreeGroup α
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
⊢ ↑(map g) (↑(map f) x) = ↑(map (g ∘ f)) x
rcases x with ⟨L⟩