proposition: Lemma BVxor_comm : forall n (v1 v2 : Bvector n), BVxor n v1 v2 = BVxor n v2 v1.
proof: Proof. induction n; intuition. rewrite (vector_0 v1). rewrite (vector_0 v2). trivial. destruct (vector_S v1). destruct H. destruct (vector_S v2). destruct H0. subst. simpl. rewrite IHn. rewrite xorb_comm. trivial. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation