∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) [inst_1 : Topology.RelCWComplex C ∅] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), Topology.CWComplex.map n i = Topology.RelCWComplex.map n i