intro η
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (a : EdgePath G x₀ x₀),
    Quot.mk Reduction a ∈ H ↔
      ∃ h',
        Quot.mk Reduction a =
          (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₀
⊢ 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'