congr
case refl.refl
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ surroundEdge Γ e = surroundEdge Γ e'
case refl.refl.e_e
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u v : V
e e' : EdgeBetween G u v
hee' : e.edge = e'.edge
⊢ e = e'