proposition: Lemma bv_not_involutive: forall n (a: bitvector n), bv_eq (bv_not (bv_not a)) a = true.
proof: Proof. intros n a. unfold bv_eq. rewrite M.bv_eq_reflect. simpl. apply (@M.bv_not_involutive a); now rewrite wf. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance