proposition: Theorem xor_OTP: forall (x : Bvector n), comp_spec eq (Rnd n) (r <-$ Rnd n; ret (BVxor n x r)).
proof: Proof. eapply OTP_inf_th_sec_l; intuition. eapply BVxor_assoc. eapply BVxor_same_id. eapply BVxor_same_id. eapply BVxor_id_l. eapply comp_spec_rnd. Qed.
imports: FCF.FCF