simp [redCons_nil]
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
hyp : reduced (nil v)
⊢ reduced (redCons e (nil v))
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
hyp : reduced (nil v)
⊢ reduced (cons e (nil v))