vstd::seq

Function axiom_seq_empty

Source
pub broadcast proof fn axiom_seq_empty<A>()
Expand description
ensures
#[trigger] Seq::<A>::empty().len() == 0,