more in line with the paper formalism, path-eval just looks up, and sub-tp rules check S<:U