rw [toFuncV_defn, toFuncE_defn]
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e : Edge G x₀
⊢ toFuncV H ⟦(univ G x₀).ι e⟧ = G.ι (toFuncE H ⟦e⟧)
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e : Edge G x₀
⊢ ((univ G x₀).ι e).τ = G.ι e.nxt.edge