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