Skip to main content

lemma_seq_empty

vstd::seq

Function lemma_seq_empty 

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