{X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} →
      [T2Space X] →
        [inst : Topology.RelCWComplex C D] → (E : Topology.RelCWComplex.Subcomplex C) → Topology.RelCWComplex (↑E) D