rw [← hom_comp_eq_id]
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
⊢ (u ⤳[Γ] v) = inv (v ⤳[Γ] u)
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
⊢ ((v ⤳[Γ] u) ≫ u ⤳[Γ] v) = 𝟙 v