Function inclCopy item path

pub open spec fn incl<K, V, P: Protocol<K, V>>(a: P, b: P) -> bool

{ exists |c| P::op(a, c) == b }