proposition: Lemma bv_not_and_or: forall n a b, (size a) = n -> (size b) = n -> bv_not (bv_and a b) = bv_or (bv_not a) (bv_not b).
proof: Proof. intros n a b H0 H1. unfold bv_and in *. rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl. unfold bv_or, size, bits in *. do 2 rewrite <- not_list_length. rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl. unfold bv_not, size, bits in *. rewrite not_list_and_or. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance