pub open spec fn conjunct_shared<RA: ResourceAlgebra>(a: RA, b: RA, c: RA) -> boolExpand description
{ forall |p: RA| p.valid() && incl(a, p) && incl(b, p) ==> #[trigger] incl(c, p) }pub open spec fn conjunct_shared<RA: ResourceAlgebra>(a: RA, b: RA, c: RA) -> bool{ forall |p: RA| p.valid() && incl(a, p) && incl(b, p) ==> #[trigger] incl(c, p) }