proposition: Lemma bv_not_size: forall n a, (size a) = n -> size (bv_not a) = n.
proof: Proof. intros n a H. unfold bv_not. unfold size, bits in *. rewrite <- not_list_length. exact H. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance