proposition: Lemma BV_to_nat_app2 : forall l n : BV, BV_to_nat (appbv l n) = BV_to_nat l + power2 (lengthbv l) * BV_to_nat n.
proof: Proof. intros. apply BV_to_nat_app. auto. unfold lenbv, lengthbv in |- *. apply len_length. Qed.
imports: Arith_compl Bool_compl Lists_replace