apply reducedConcat_cancel_pair
case p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ e.p:+e.nxt:+EdgeBetween.bar e.nxt = e.p
case p.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ reduced e.p