proposition: Lemma bv_zextn_size: forall n (i: N) a, size a = n -> size (@bv_zextn n i a) = (i + n)%N.
proof: Proof. intros. unfold bv_zextn, zextend, size in *. rewrite <- N2Nat.id. apply f_equal. specialize (@length_extend a (nat_of_N i) false). intros. rewrite H0. rewrite plus_distr. rewrite plus_comm. apply f_equal. apply (f_equal (N.to_nat)) in H. now rewrite Nat2N.id in H. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance