intro red p' red'
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
⊢ reduced (cons e p) → reduced p
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