proposition: Lemma bv_and_comm n a b : size a = n -> size b = n -> bv_and a b = bv_and b a.
proof: Proof. intros H1 H2. unfold bv_and. rewrite H1, H2. rewrite N.eqb_compare, N.compare_refl. rewrite map2_and_comm. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance