have : e' = e''.bar := by
  ext
  rw [EdgeBetween.bar_eq_bar]
  rw [← leqn.1, leqn.2.1]
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 (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList 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
hyp : reduced (cons e' p')
c' : ¬e' = EdgeBetween.bar e''
p'' : EdgePath G u✝ w
red' : Reduction (cons e'' (cons e' p')) p''
u u' : V
p₁ : EdgePath G u✝ u
e : EdgeBetween G u✝ u'
p₂ : EdgePath G u✝ w
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e'' (cons e' p')
leqn : e.edge = e''.edge ∧ G.bar e.edge = e'.edge ∧ toList p₂ = toList p'
this : e' = EdgeBetween.bar e''
⊢ False