Allow specifying types in separate files

[nano-o]

In some contexts it's desirable to be able to check an existing specification with Apalache without changing at all the existing specification.

Let's say the existing specification is Spec.tla. We can create a new spec ApaSpec.tla that declares the same variables as Spec.tla but with type annotations and instantiates Spec.tla. However, if type annotations on other expressions are needed, there seem to be no way to put them in ApaSpec.tla.

An example is discussed in this PR: tlaplus/Examples#113. We need an annotation on vars in Einstein.tla and there seem to be no way to put this annotation in a different file.