Function inclCopy item path

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

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