proposition: Lemma bv_sextn_size: forall n (i: N) a, size a = n -> size (@bv_sextn n i a) = (i + n)%N.
proof: Proof. intros. unfold bv_sextn, sextend, size in *. rewrite <- N2Nat.id. apply f_equal. case_eq a. intros. rewrite length_mk_list_false. rewrite H0 in H. simpl in H. rewrite <- H. lia. intros. specialize (@length_extend a (nat_of_N i) b). intros. subst. rewrite plus_distr. rewrite plus_comm. rewrite Nat2N.id. now rewrite <- H1. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance