proposition: Lemma bv_concat_size n m a b : size a = n -> size b = m -> size (bv_concat a b) = (n + m)%N.
proof: Proof. unfold bv_concat, size. intros H0 H1. rewrite app_length, Nat2N.inj_add, H0, H1; now rewrite N.add_comm. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance