apply Quot.ind
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (p : PathClass G u v), mul p (PathClass.id v) = p
case mk
V : Type u
E : Type v
G : Graph V E
u✝ v✝ w : V
e : EdgeBetween G v✝ w
u v : V
⊢ ∀ (a : EdgePath G u v), mul (Quot.mk Reduction a) (PathClass.id v) = Quot.mk Reduction a