proposition: Theorem comp_spec_rnd : forall n x y, comp_spec (fun a b : Vector.t bool n => a = x <-> b = y) ({ 0 , 1 }^n) ({ 0 , 1 }^n).
proof: Proof. intuition. eapply eq_impl_comp_spec; wftac. eapply uniformity. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1