let θ₁ := η₁.lift p v₁ h
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₂ w₂' u₂ : V₂
h : p.toFuncV v₁ = v₂
η₁ : EdgePath G₂ v₂ w₂
e : EdgeBetween G₂ w₂ w₂'
η₂ : EdgePath G₂ w₂ u₂
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)
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₂ w₂' u₂ : V₂
h : p.toFuncV v₁ = v₂
η₁ : EdgePath G₂ v₂ w₂
e : EdgeBetween G₂ w₂ w₂'
η₂ : EdgePath G₂ w₂ u₂
θ₁ : PathLift p v₁ h η₁ := lift η₁ p v₁ h
⊢ PathLift.pathClass (lift (η₁ ++ cons e (cons (EdgeBetween.bar e) η₂)) p v₁ h) =
    PathLift.pathClass (lift (η₁ ++ η₂) p v₁ h)