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