∀ {E : Type u_1} {X : Type u_3} {A : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) {f₀ f₁ : C(A, X)} {S : Set A}
  (F : f₀.HomotopyRel f₁ S) {f₀' : C(A, E)} (F_0 : ∀ (a : A), F (0, a) = p (f₀' a)) (t : ↑unitInterval),
  ∀ a ∈ S, (cov.liftHomotopy (↑F) f₀' F_0) (t, a) = f₀' a