proposition: Lemma length_amapi : forall {A B} (f:int -> A -> B) t, length (amapi f t) = length t.
proof: Proof. unfold amapi; intros A B f t. assert (Bt := to_Z_bounded (length t)). apply (foldi_ind _ (fun _ a => length a = length t)). apply leb_0. rewrite length_make, leb_length by reflexivity; reflexivity. intros i a _; assert (Bi := to_Z_bounded i). rewrite ltb_spec; intros Hi IH. rewrite length_set; exact IH. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz