proposition: Lemma bv_and_empty_empty1: forall a, (bv_and a bv_empty) = bv_empty.
proof: Proof. intros a. unfold bv_empty, bv_and, size, bits. simpl. rewrite map2_and_empty_empty1. case_eq (N.compare (N.of_nat (length a)) 0); intro H; simpl. - apply (N.compare_eq (N.of_nat (length a))) in H. rewrite H. simpl. reflexivity. - rewrite N.eqb_compare. rewrite H; reflexivity. - rewrite N.eqb_compare. rewrite H; reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance