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