pub broadcast proof fn lemma_seq_empty_contains_nothing<A>(x: A)Expand description
ensures
!(#[trigger] Seq::<A>::empty().contains(x)),The empty sequence contains nothing
pub broadcast proof fn lemma_seq_empty_contains_nothing<A>(x: A)!(#[trigger] Seq::<A>::empty().contains(x)),The empty sequence contains nothing