Function vstd::set::axiom_set_empty

pub broadcast proof fn axiom_set_empty<A>(a: A)

Expand description

ensures

!(#[trigger] Set::empty().contains(a)),

The empty set contains no elements

Function vstd::set::axiom_set_emptyCopy item path