proposition: Lemma bv_xor_1_true: forall a, (bv_xor a (mk_list_true (length (bits a)))) = map negb a.
proof: Proof. intro a. unfold bv_xor. rewrite N.eqb_compare. unfold size, bits. rewrite length_mk_list_true. rewrite N.compare_refl. rewrite map2_xor_1_true. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance