apply redCons_eq_cons_of_reduced
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ redCons e p = cons e p
case cons.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ reduced (cons e p)