proposition: Theorem RndNat_eq_any : forall (eta : nat)(x : Bvector eta), Pr [a0 <-$ { 0 , 1 }^eta; ret (eqb x a0) ] == 1 / 2^eta.
proof: Proof. intuition. simpl. rewrite (@sumList_exactly_one _ x). rewrite eqbBvector_complete. destruct (EqDec_dec bool_EqDec true true); intuition. rewrite ratMult_1_r. reflexivity. eapply getAllBvectors_NoDup. apply in_getAllBvectors. intuition. destruct (EqDec_dec bool_EqDec (eqbBvector x b) true); intuition. apply eqbBvector_sound in e. intuition. eapply ratMult_0_r. Qed.
imports: FCF.FCF