symm at eqn
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✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' 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✝
u w✝ : V
ph : EdgeBetween G u✝¹ w✝
pt : EdgePath G w✝ u
e : EdgeBetween G u u'
p₂ : EdgePath G u w
eqn : cons e✝ (cons e' p') = cons ph pt ++ cons e (cons (EdgeBetween.bar e) p₂)
⊢ False