induction p <;> aesop (add norm simp [Graph.EdgePath.reverse])
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v : V
p : Graph.EdgePath Γ u v
⊢ pathLabel 𝓖 (Graph.EdgePath.reverse p) = (pathLabel 𝓖 p)⁻¹
no goals