intro p'
case mk.mk
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
⊢ ∀ (a : Graph.EdgePath Γ v w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ Quot.mk Graph.EdgePath.Reduction a) =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a)
case mk.mk
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
⊢ pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ Quot.mk Graph.EdgePath.Reduction p') =
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p')