proposition: Lemma bv_add_twice: forall a, bv_add a a = removelast (false :: a).
proof: Proof. intro a. unfold bv_add, size, bits. rewrite N.eqb_compare. rewrite N.compare_refl. rewrite add_list_twice. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance