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