intro η₁
case refl.mk
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst : CoveringMap p
v₁ : V₁
⊢ ∀ (a : EdgePath G₁ v₁ v₁) ⦃a₂ : π₁ G₁ v₁⦄,
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction a) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) a₂ →
      Quot.mk Reduction a = a₂
case refl.mk
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst : CoveringMap p
v₁ : V₁
η₁ : EdgePath G₁ v₁ v₁
⊢ ∀ ⦃a₂ : π₁ G₁ v₁⦄,
    (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) (Quot.mk Reduction η₁) =
        (Morphism.π₁map v₁ (p.toFuncV v₁) p (_ : p.toFuncV v₁ = p.toFuncV v₁)) a₂ →
      Quot.mk Reduction η₁ = a₂