proposition: Lemma to_list_amap : forall A B (f : A -> B) t, to_list (amap f t) = List.map f (to_list t).
proof: Proof. intros A B f t. assert (Bt := to_Z_bounded (length t)). unfold to_list; rewrite length_amap. rewrite map_rev; f_equal. apply (foldi_ind2 _ _ (fun i a b => a = map f b)). apply leb_0. reflexivity. intros i a1 a2 _; assert (Bi := to_Z_bounded i). rewrite ltb_spec; intros Hi IH. simpl; f_equal. apply get_amap. rewrite ltb_spec; lia. apply IH. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz