let ⟨t', h₁', h₂'⟩ := h'
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
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
h' : ∃ t_1, t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t_1 ∧ redCons (EdgeBetween.bar e) t = t_1
⊢ redCons (EdgeBetween.bar e) t = cons (EdgeBetween.bar 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
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
h' : ∃ t_1, t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t_1 ∧ redCons (EdgeBetween.bar e) t = t_1
t' : EdgePath G v w
h₁' : t = cons (EdgeBetween.bar (EdgeBetween.bar e)) t'
h₂' : redCons (EdgeBetween.bar e) t = t'
⊢ redCons (EdgeBetween.bar e) t = cons (EdgeBetween.bar e) t