pub fn axiom_seq_new_len<A>(len: nat, f: FnSpec<(int,), A>)
Seq axioms have been verified, and are now lemmas
#[trigger] Seq::new(len, f).len() == len,