∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {γ : C(↑unitInterval, X)} {e : E} (γ_0 : γ 0 = p e) {Γ : ↑unitInterval → E},
  Γ = ⇑(cov.liftPath γ e γ_0) ↔ Continuous Γ ∧ p ∘ Γ = ⇑γ ∧ Γ 0 = e