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