∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.closedCell n j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)