pub proof fn seq_tracked_update<T>(s: Seq<T>, idx: int, x: T) -> tracked res : Seq<T>Expand description
requires
0 <= idx < s.len(),res == s.update(idx, x),pub proof fn seq_tracked_update<T>(s: Seq<T>, idx: int, x: T) -> tracked res : Seq<T>0 <= idx < s.len(),res == s.update(idx, x),