apply lifts_homotopic p p₁' p₂'
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₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ toList p₁' = toList p₂'
case hv
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₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ w✝¹ = w✝

case a
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₂')
edg_eq : edg₁.edge = edg₂.edge
⊢ List.map p.toFuncE (toList p₁') = List.map p.toFuncE (toList p₂')