simp [redCons, h]
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v v' w : V
e : EdgeBetween G u v
e' : EdgeBetween G v v'
p : EdgePath G v' w
h : v' ≠ u
⊢ redCons e (cons e' p) = cons e (cons e' p)
no goals