proposition: Lemma get_amapi : forall {A B} (f:int -> A -> B) t i, i <? length t = true -> (amapi f t).[i] = f i (t.[i]).
proof: Proof. intros A B f t. assert (Bt := to_Z_bounded (length t)). intro i; assert (Bi := to_Z_bounded i). rewrite ltb_spec; intro Hi. generalize (length_amapi f t); unfold amapi; revert Hi. set (a := foldi _ _ _ _); pattern (length t) at 1, a; subst a; apply foldi_ind. rewrite leb_spec, to_Z_0; lia. rewrite to_Z_0; lia. intros j a _; assert (Bj := to_Z_bounded j). rewrite ltb_spec; intros Hj IH. rewrite to_Z_add_1_wB by lia; intro Hij. rewrite length_set; case (reflect_eqb j i); [ intro Heq; rewrite Heq | intro Hneq ]; intro Hlength. rewrite get_set_same by (rewrite Hlength, ltb_spec; lia); reflexivity. rewrite get_set_other by exact Hneq. apply IH; [ rewrite <- to_Z_eq in Hneq; lia | exact Hlength ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz