congr
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₂
v₁✝ w₁✝ v₂ w₂✝ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁✝ w₁✝
e₂ : EdgePath G₁ v₂ w₂✝
w₁ v₁ w✝¹ : V₁
edg₁ : EdgeBetween G₁ v₁ w✝¹
p₁' : EdgePath G₁ w✝¹ w₁
hv : v₁ = v₂
w₂ w✝ : V₁
edg₂ : EdgeBetween G₁ v₁ w✝
p₂' : EdgePath G₁ w✝ w₂
hyp : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge ∧ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
h₁ : p.toFuncE edg₁.edge = p.toFuncE edg₂.edge
h₂ : List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')
eq₁ : Morphism.localSection p v₁ (p.toFuncE edg₁.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₁.edge)) = edg₁.edge :=
  Morphism.localSection_toFuncE p v₁ edg₁.edge edg₁.init_eq.symm
eq₂ : Morphism.localSection p v₁ (p.toFuncE edg₂.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₂.edge)) = edg₂.edge :=
  Morphism.localSection_toFuncE p v₁ edg₂.edge edg₂.init_eq.symm
⊢ Morphism.localSection p v₁ (p.toFuncE edg₁.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₁.edge)) =
    Morphism.localSection p v₁ (p.toFuncE edg₂.edge) (_ : p.toFuncV v₁ = G₂.ι (p.toFuncE edg₂.edge))
no goals