proposition: Lemma bv_not_false_true: forall n, bv_not (mk_list_false n) = (mk_list_true n).
proof: Proof. intros n. unfold bv_not. unfold size, bits. rewrite not_list_false_true. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance