pub proof fn seq_tracked_subrange<T>(s: Seq<T>, start: int, end: int) -> tracked res : Seq<T>Expand description
requires
0 <= start <= end <= s.len(),res == s.subrange(start, end),