pub proof fn seq_tracked_map_values<T, U>(s: Seq<T>, f: FnSpec<(T,), U>) -> tracked res : Seq<U>
res == s.map_values(f),