proposition: Lemma BVxor_id_r_inv : forall n (v1 v2 : Bvector n), BVxor n v1 v2 = v1 -> v2 = (Bvect_false n).
proof: Proof. intuition. rewrite <- BVxor_id_l at 1. rewrite <- (BVxor_same_id v1). rewrite BVxor_assoc. f_equal; intuition. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation