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