proposition: Lemma BVxor_same_id : forall n (v : Bvector n), BVxor n v v = Bvect_false n.
proof: Proof. induction n; intuition. rewrite (vector_0 v). simpl. unfold Bvect_false. simpl. trivial. destruct (vector_S v). destruct H. rewrite H. unfold Bvect_false. simpl. rewrite IHn. rewrite xorb_nilpotent. trivial. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation