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 : v ⟶ w) (q : w ⟶ u) (r : 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 : w ⟶ u) (r : u ⟶ u'), (Quot.mk Reduction a ≫ q) ≫ r = Quot.mk Reduction a ≫ q ≫ r