let η' := reduction η
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
⊢ Quot.mk Reduction η ∈ H ↔
    ∃ h',
      Quot.mk Reduction η =
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          h'
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
⊢ Quot.mk Reduction η ∈ H ↔
    ∃ h',
      Quot.mk Reduction η =
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          h'