induction p <;> aesop (add norm simp [mul_assoc])
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
p' : Graph.EdgePath Γ v w
⊢ pathLabel 𝓖 (p ++ p') = pathLabel 𝓖 p * pathLabel 𝓖 p'
no goals