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