proposition: Theorem uniformity : forall n (x1 x2 : Bvector n), evalDist ({0, 1} ^ n) x1 == evalDist ({0, 1} ^ n) x2.
proof: Proof. intuition. unfold evalDist. eapply eqRat_refl. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia