5.11 Module Import

Notation 4 / rule 2
fs:local-variables(statEnv2, URILiteral)
fs:local-functions(statEnv2, URILiteral)
    I think there's a missing connection between dynEnv2 in the conclusion
    and statEnv2 in the premises.

SCP / rule (1|2)
URILiteral1 =>module_statEnv statEnv1
...
URILiteral1 =>module_statEnv statEnvn
    The prose says that these premises look up the static contexts of
    all the imported modules. However, this doesn't really work...

    1) There's no guarantee that it hits all importable modules. (E.g.,
       the inference process can pick n=1 and satisfy the rule with just
       one module, regardless of the number that could have satisfied it.)

    2) Even if we assume that the inference process somehow knows the
       "right" value for n, there's still no guarantee that it will bind
       the statEnvs to n distinct environments (from n different modules),
       since there's no requirement that the statEnvi be distinct.

    In either case, the inference process can deduce the wrong statEnvn'.

    Instead, I repeat my suggestion (from Bug 1704) to introduce a
    function like fs:library-modules-with-target-namespace(N).

DCP / rule 1
    Similarly.