induction p with
| nil _ => simp only [surround, Subgraph.contains_nil, SpanningSubgraph.spanning, Set.top_eq_univ, Set.mem_univ,
  Graph.PathClass.nil_eq_id, path_to_base_eq, Category.id_comp, IsIso.hom_inv_id, surroundEdgewise_nil]
| cons _ _ ih => simp only [surroundEdgewise_cons, ← ih, surround_cons]
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
p : EdgePath G u v
⊢ surround Γ [[p]] = surroundEdgewise Γ p
no goals