apply redCons_cons_edge_eq
case inl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
hyp : reduced p
h : redCons e p = cons e p
⊢ redCons (EdgeBetween.bar e) (cons e p) = p
case inl.h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
hyp : reduced p
h : redCons e p = cons e p
⊢ e = EdgeBetween.bar (EdgeBetween.bar e)