{X : Type u} →
  [inst : TopologicalSpace X] →
    {C D : Set X} →
      {motive : Topology.RelCWComplex C D → Sort u_1} →
        ((cell : ℕ → Type u) →
            (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) →
              (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) →
                (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) →
                  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) →
                    (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) →
                      (disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D) →
                        (mapsTo :
                            ∀ (n : ℕ) (i : cell n),
                              ∃ I,
                                Set.MapsTo (↑(map n i)) (Metric.sphere 0 1)
                                  (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' Metric.closedBall 0 1)) →
                          (closed' :
                              ∀ A ⊆ C,
                                (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) ∧
                                    IsClosed (A ∩ D) →
                                  IsClosed A) →
                            (isClosedBase : IsClosed D) →
                              (union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) →
                                motive
                                  { cell := cell, map := map, source_eq := source_eq, continuousOn := continuousOn,
                                    continuousOn_symm := continuousOn_symm, pairwiseDisjoint' := pairwiseDisjoint',
                                    disjointBase' := disjointBase', mapsTo := mapsTo, closed' := closed',
                                    isClosedBase := isClosedBase, union' := union' }) →
          (t : Topology.RelCWComplex C D) → motive t