extra application of discrete_topology

Author: zstone1

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) => //.