aesop
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
u v : V
⊢ ∀ (a : EdgePath G u v), Quot.mk Reduction a ≫ 𝟙 v = Quot.mk Reduction a
no goals