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