rw [←eqn, ← cons_append] at hyp
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''
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = p'
⊢ False
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
c' : e' = EdgeBetween.bar e✝
p'' : EdgePath G u✝ w
red' : Reduction p' p''
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u w
hyp : reduced (cons e' p₁ ++ cons e (cons (EdgeBetween.bar e) p₂))
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = p'
⊢ False