pub broadcast proof fn lemma_seq_all_index<T>(s: Seq<T>, f: FnSpec<(T,), bool>, i: int)Expand description
requires
0 <= i < s.len(),#[trigger] s.all(f),f(#[trigger] (s[i])),Index i of the sequence s satisfies f(s[i]) if s.all(f) holds.
This proof is required due to the change of trigger by replacing the original forall_seq_values with Seq::all.