rw [nil_append] at eqn
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e✝ : EdgeBetween G u v
p' : EdgePath G u v
red' : Reduction (cons e✝ (nil v)) p'
u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
eqn : nil u ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (nil v)
⊢ False
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e✝ : EdgeBetween G u v
p' : EdgePath G u v
red' : Reduction (cons e✝ (nil v)) p'
u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (nil v)
⊢ False