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