cases prepend_cases e p with
| inl h =>
    rw [h]
    apply redCons_cons_edge_eq
    simp [bar_bar]
| inr h =>
    let ⟨t, h₁, h₂⟩ := h
    rw[h₂, h₁]
    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
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
⊢ redCons (EdgeBetween.bar e) (redCons e p) = p
no goals