cases prepend_cases e.bar t with
| inl h' =>
  assumption
| inr h' =>
  let ⟨t', h₁', h₂'⟩ := h'
  rw [h₂', h₁']
  rw [h₁, h₁'] at hyp
  simp [bar_bar] at *
  have split :
            cons e.bar (cons e t') =
              (nil v : EdgePath G v v) ++
                cons e.bar (cons e.bar.bar t') := by
              simp [nil_append]
  have :¬ reduced (cons e.bar (cons e t')) := by
    apply not_reduced_of_split split
  contradiction
case inr
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 p
h : ∃ t, p = cons (EdgeBetween.bar e) t ∧ redCons e p = t
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
⊢ redCons (EdgeBetween.bar e) t = cons (EdgeBetween.bar e) t
no goals