simp [nil_toList] at *
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₂
v : V₁
x✝ : v₁ = v
hyp : List.map p.toFuncE (toList (cons edg₁ p₁')) = List.map p.toFuncE (toList (nil v))
⊢ toList (cons edg₁ p₁') = toList (nil v)
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₂
v : V₁
x✝ : v₁ = v
hyp : toList (cons edg₁ p₁') = []
⊢ toList (cons edg₁ p₁') = []