induction p with
  | nil _ => simp
  | cons _ _ ih => simp_all [ih]
V : Type u_3
E : Type u_1
X : Graph V E
Γ : SpanningSubtree X
G : Type ?u.113042
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
p : EdgePath X u v
hpΓ : Subgraph.contains Γ.toSubgraph p
⊢ GroupLabelledGraph.pathLabel (SpanningSubtree.edgeLabelExtension φ) p = 1
no goals