intro p' red'
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v : V
e : EdgeBetween G u v
⊢ reduced (cons e (nil v))
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'
⊢ False