show (Γ.edgeLabelExtension φ).pathClassLabel ([[_]]) = _
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.116565
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
inst✝ : {u v : V} → (e : EdgeBetween X u v) → Decidable (e.edge ∈ Γ.edges)
φ : ↑Γ.edgesᶜ →⁻¹ H
u v : V
⊢ GroupLabelledGraph.pathClassLabel (SpanningSubtree.edgeLabelExtension φ) (u ⤳[Γ] v) = 1
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.116565
inst✝² : Group G
H : Type u_2
inst✝¹ : Group H
inst✝ : {u v : V} → (e : EdgeBetween X u v) → Decidable (e.edge ∈ Γ.edges)
φ : ↑Γ.edgesᶜ →⁻¹ H
u v : V
⊢ GroupLabelledGraph.pathClassLabel (SpanningSubtree.edgeLabelExtension φ)
      [[↑((SpanningSubtree.toSubtree Γ).toPreconnectedSubgraph.path (SpanningSubtree.vertex_coe Γ u)
            (SpanningSubtree.vertex_coe Γ v))]] =
    1