simp only [redCons_nil, false_and, exists_false, or_false]
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
⊢ redCons e (nil v) = cons e (nil v) ∨ ∃ t, nil v = cons (EdgeBetween.bar e) t ∧ redCons e (nil v) = t
no goals