Function vstd::seq::axiom_seq_new_index
source · pub broadcast proof fn axiom_seq_new_index<A>(len: nat, f: FnSpec<(int,), A>, i: int)Expand description
requires
0 <= i < len,#[trigger] Seq::new(len, f)[i] == f(i),