exact lem
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₁ w₁ : V₁
e₁ e₂ : EdgePath G₁ v₁ w₁
hyp : [[EdgePath.map e₁ p]] = [[EdgePath.map e₂ p]]
lem : [[e₁]] = [[e₂]]
⊢ [[e₁]] = [[e₂]]
no goals