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