simp only [surround, path_to_base_eq, Category.assoc, IsIso.inv_hom_id_assoc]
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v w : V
p : u ⟶ v
q : v ⟶ w
⊢ surround Γ p ≫ surround Γ q = surround Γ (p ≫ q)
no goals