Function vstd::seq::axiom_seq_subrange_len
source · pub broadcast proof fn axiom_seq_subrange_len<A>(s: Seq<A>, j: int, k: int)Expand description
requires
0 <= j <= k <= s.len(),#[trigger] s.subrange(j, k).len() == k - j,