rename_i w' w''
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 w✝ : V
e' : EdgeBetween G v w✝
p' : EdgePath G w✝ w
hyp : reduced (cons e' p')
⊢ reduced (redCons e (cons e' p'))
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 w'' : V
e' : EdgeBetween G v w''
p' : EdgePath G w'' w
hyp : reduced (cons e' p')
⊢ reduced (redCons e (cons e' p'))