uniform_compose@{} mu {Eg : Uniform g mu} mu' {Ef : Uniform f mu'} : Uniform (Compose g f) (Compose mu' mu). Proof. intros e u v xi. unfold Compose. apply (uniform g _),(uniform f _),xi. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.