Function lemma_seq_new_len Copy item path

pub broadcast proof fn lemma_seq_new_len<A>(len: nat, f: FnSpec<(int,), A>)

#[trigger] Seq::new(len, f).len() == len,