intro p₁ p₂
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₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
⊢ ∀ (p₁ : PathLift p v₁ h₁ e) (p₂ : PathLift p v₁ h₂ e), p₁ = p₂
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₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
⊢ p₁ = p₂