proposition: Lemma BVxor_id_l : forall n (v : Bvector n), BVxor n (Bvect_false n) v = v.
proof: Proof. intuition. rewrite BVxor_comm. apply BVxor_id_r. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation