diff --git a/theories/cantor.v b/theories/cantor.v
index fdf5bca498..2384c774d3 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -484,7 +484,7 @@ Local Lemma cantor_surj_pt1 : exists2 f : Tree -> T,
 Proof.
 pose entn n := projT2 (cid (ent_balls' (count_unif n))).
 have [ | |? []//| |? []// | |] := @tree_map_props
-    (discrete_topology \o K) T (embed_refine) (embed_invar) cptT hsdfT.
+    K T (embed_refine) (embed_invar) cptT hsdfT.
 - move=> n U; rewrite eqEsubset; split=> [t Ut|t [? ? []]//].
   have [//|_ _ _ + _] := entn n; rewrite -subTset.
   move=> /(_ t I)[W cbW Wt]; exists (existT _ W cbW) => //.