rfl
case τ₀
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.τ₀ =
    e.τ₀
no goals