pub proof fn lemma_forall_seq_index<T>(s: Seq<T>, f: FnSpec<(int, T), bool>, i: int)Expand description
requires
forall_seq(s, f),0 <= i < s.len(),f(i, s[i]),Index i of the sequence s satisfies f(i,s[i]) if forall_seq(s,f) holds.