Could be based on `beyond.v` + subset operation (e.g. see https://hackage.haskell.org/package/containers-0.6.6/docs/src/Data.Set.Internal.html#isSubsetOfX)