proposition: Lemma bv_not_involutive: forall a, bv_not (bv_not a) = a.
proof: Proof. intro a. unfold bv_not. unfold size, bits. rewrite not_list_involutative. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance