cases this
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w v' w' : V
e : EdgeBetween G u v
p : EdgePath G v w
ph : EdgeBetween G u v'
pt : EdgePath G v' w'
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
this : v' = v
⊢ ¬reduced p
case refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
u' : V
G : Graph V E
u v w w' : V
e : EdgeBetween G u v
p : EdgePath G v w
e' : EdgeBetween G w' u'
p₂ : EdgePath G w' w
ph : EdgeBetween G u v
pt : EdgePath G v w'
hyp : cons e p = cons ph (pt ++ cons e' (cons (EdgeBetween.bar e') p₂))
lhyp : e.edge = ph.edge ∧ toList p = toList pt ++ e'.edge :: G.bar e'.edge :: toList p₂
⊢ ¬reduced p