vstd::storage_protocol

Function incl

Source 
pub open spec fn incl<K, V, P: Protocol<K, V>>(a: P, b: P) -> bool
Expand description
{ exists |c| P::op(a, c) == b }