rw [← surroundEdge_bar]
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
e : E
⊢ surroundEdge Γ (EdgeBetween.ofEdge (G.bar e)) = inv (surroundEdge Γ (EdgeBetween.ofEdge e))
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
e : E
⊢ surroundEdge Γ (EdgeBetween.ofEdge (G.bar e)) = surroundEdge Γ (EdgeBetween.bar (EdgeBetween.ofEdge e))