erw [Graph.EdgePath.cons_eq_append_singletonPath, surround_append]
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
v✝ w✝ : V
e : EdgeBetween G v✝ w✝
a✝ : V
p : EdgePath G w✝ a✝
⊢ surround Γ [[EdgePath.cons e p]] = surroundEdge Γ e ≫ surround Γ [[p]]
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
v✝ w✝ : V
e : EdgeBetween G v✝ w✝
a✝ : V
p : EdgePath G w✝ a✝
⊢ surround Γ [[singletonPath e ++ p]] = surround Γ ([[singletonPath e]] ≫ [[p]])