apply Quot.ind
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (p : PathClass G v w) (q : PathClass G w u) (r : PathClass G u u'), p * q * r = p * (q * r)
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e : EdgeBetween G v✝ w✝
v w u u' : V
⊢ ∀ (a : EdgePath G v w) (q : PathClass G w u) (r : PathClass G u u'),
    Quot.mk Reduction a * q * r = Quot.mk Reduction a * (q * r)