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]
case inr.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
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
t' : EdgePath G v w
h₂' : redCons (EdgeBetween.bar e) t = t'
h : p = cons (EdgeBetween.bar e) (redCons e p)
h' : t = cons e (redCons (EdgeBetween.bar e) t)
hyp : reduced (cons (EdgeBetween.bar e) (cons e t'))
h₁' : t = cons e t'
⊢ t' = cons (EdgeBetween.bar e) (cons e t')
case inr.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
t : EdgePath G u w
h₁ : p = cons (EdgeBetween.bar e) t
h₂ : redCons e p = t
t' : EdgePath G v w
h₂' : redCons (EdgeBetween.bar e) t = t'
h : p = cons (EdgeBetween.bar e) (redCons e p)
h' : t = cons e (redCons (EdgeBetween.bar e) t)
hyp : reduced (cons (EdgeBetween.bar e) (cons e t'))
h₁' : t = cons e t'
split :
  cons (EdgeBetween.bar e) (cons e t') =
    nil v ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) t')
⊢ t' = cons (EdgeBetween.bar e) (cons e t')