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