proposition: Lemma bv_and_empty_empty2: forall a, (bv_and bv_empty a) = bv_empty.
proof: Proof. intro a. unfold bv_and, bv_empty, size. case (length a); simpl; auto. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance