have teq : τ₁ = τ₂ := term_eq
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
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
τ₂ : V₁
path₂ : EdgePath G₁ v₁ τ₂
h₂ : p.toFuncV τ₂ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
⊢ { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ } =
    { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }
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
τ₁ : V₁
path₁ : EdgePath G₁ v₁ τ₁
h₁ : p.toFuncV τ₁ = w₂
lc₁ : List.map p.toFuncE (toList path₁) = toList e
τ₂ : V₁
path₂ : EdgePath G₁ v₁ τ₂
h₂ : p.toFuncV τ₂ = w₂
lc₂ : List.map p.toFuncE (toList path₂) = toList e
eq_edgepath_aux :
  List.map p.toFuncE (toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path) =
    List.map p.toFuncE (toList { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path)
eq_edgepath :
  toList { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.path =
    toList { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.path
term_eq :
  { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ }.τ =
    { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }.τ
teq : τ₁ = τ₂
⊢ { τ := τ₁, path := path₁, term_pushdown := h₁, list_pushdown := lc₁ } =
    { τ := τ₂, path := path₂, term_pushdown := h₂, list_pushdown := lc₂ }