uniform_continuous@{} mu `{!Uniform@{UA UB} f mu} : Continuous f. Proof. hnf. intros u e;apply tr;exists (mu e). apply (uniform f mu). Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.