let ⟨u, u', e', p₁, p₂, eqn⟩   := red'.property
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G v✝ w✝
u v w : V
e : EdgeBetween G u v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction 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 v✝ w✝
u✝ v w : V
e : EdgeBetween G u✝ v
p : EdgePath G v w
red : reduced (cons e p)
p' : EdgePath G v w
red' : Reduction p p'
u u' : V
e' : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e' (cons (EdgeBetween.bar e') p₂) = p
⊢ False