simp only [surroundEdgewise_cons, ← ih, surround_cons]
case cons
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v v✝ w✝ u✝ : V
a✝¹ : EdgeBetween G v✝ w✝
a✝ : EdgePath G w✝ u✝
ih : surround Γ [[a✝]] = surroundEdgewise Γ a✝
⊢ surround Γ [[EdgePath.cons a✝¹ a✝]] = surroundEdgewise Γ (EdgePath.cons a✝¹ a✝)
no goals