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