proposition: Lemma bv_xor_empty_empty1: forall a, (bv_xor a bv_empty) = bv_empty.
proof: Proof. intros a. unfold bv_empty. unfold bv_xor, bits, size. simpl. case_eq (N.compare (N.of_nat (length a)) 0); intro H; simpl. - apply (N.compare_eq (N.of_nat (length a)) 0) in H. rewrite H. simpl. rewrite map2_xor_empty_empty1; 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