proposition: Theorem xor_1_1 : forall (n : nat)(x y z : Bvector n), BVxor _ y x = BVxor _ z x -> y = z.
proof: Proof. intuition. rewrite <- BVxor_id_r at 1. rewrite <- (BVxor_same_id x). rewrite <- BVxor_assoc. rewrite H. rewrite BVxor_assoc. rewrite (BVxor_same_id x). rewrite BVxor_id_r. trivial. Qed.
imports: FCF PRF SplitVector HMAC_spec