proposition: Lemma bv_and_size n a b : size a = n -> size b = n -> size (bv_and a b) = n.
proof: Proof. unfold bv_and. intros H1 H2. rewrite H1, H2. rewrite N.eqb_compare. rewrite N.compare_refl. unfold size in *. rewrite <- map2_and_length. - exact H1. - unfold bits. now rewrite <- Nat2N.inj_iff, H1. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance