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'
w w'' : V
e' : EdgeBetween G v w''
p' : EdgePath G w'' w
⊢ redCons e (cons e' p') = cons e (cons e' p') ∨
    ∃ t, cons e' p' = cons (EdgeBetween.bar e) t ∧ redCons e (cons e' p') = t
no goals