Function seq_tracked_new Copy item path

pub proof fn seq_tracked_new<T>(len: nat, f: impl Fn(int) -> T) -> tracked res : Seq<T>

res == Seq::<T>::new(len, f),