match p with
| nil _ =>
  simp only [redCons_nil, false_and, exists_false, or_false]
| cons e' p' =>
  rename_i w' w''
  if c:w'' = u then
    cases c
    if c':e' = e.bar
      then
        simp [redCons_cons_edge_eq p' c']
        simp only [c', or_true]
      else
        simp [redCons_cons_edge_neq p' c']
  else
    simp only [redCons_cons_vertex_neq e e' p' c, cons.injEq, exists_eq_right', true_or]
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 p = cons e p ∨ ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
no goals