∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {e : Y → X} (x : Y) (x_1 : Set X)
  (motive : x_1 ∈ nhds (e x) ∧ ContractibleSpace ↑x_1 ∧ x_1 ⊆ Set.range e → Prop)
  (x_2 : x_1 ∈ nhds (e x) ∧ ContractibleSpace ↑x_1 ∧ x_1 ⊆ Set.range e),
  (∀ (left : x_1 ∈ nhds (e x)) (hs : ContractibleSpace ↑x_1) (hse : x_1 ⊆ Set.range e), motive ⋯) → motive x_2