let leqn := congrArg EdgePath.toList eqn
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = nil v
leqn : toList (cons e (cons (EdgeBetween.bar e) p₂)) = toList (nil v) := congrArg toList eqn
⊢ False