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