intro p'' red'
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'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
hyp : reduced (cons e' p')
c' : e' = EdgeBetween.bar e
⊢ reduced p'
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'
w : V
e' : EdgeBetween G v u
p' : EdgePath G u w
hyp : reduced (cons e' p')
c' : e' = EdgeBetween.bar e
p'' : EdgePath G u w
red' : Reduction p' p''
⊢ False