{X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} →
      [inst : Topology.RelCWComplex C D] →
        (E : Topology.RelCWComplex.Subcomplex C) →
          (F : Set X) →
            F = ↑E → (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) → J = E.I → Topology.RelCWComplex.Subcomplex C