Re: [tlaplus] theorems from instantiated modules in `tlapm` version 2

Hi Stephan,

Thanks for noting the pre-alpha status of the code. I will report further issues on GitHub.

I will note in this thread another observation, about `tlapm == 1.4.3`, due to its relevance.
If module A contains a local instantiation `Inst` (without parameters), and module B extends A,
then mentioning `Inst!SomeDef` in a proof within B works for `tlapm`, though `tla2sany` cannot
find the definition, because it is local. Parameterized instantiation is mentioned in the
unsupported features, so seems to be a related issue.

Making the instance visible avoids the errors from `tla2sany`.
Duplicating the instantiation within the proof in B works for `tla2sany`, but not for `tlapm`.
My hypothesis is that the definition in module B shadows the local one in module A.

In the development version of `tlapm`, `tla2sany` still raises errors when the instantiation
is local, but it generates XML output, so `tlapm` proceeds (with a later error due to absence
of `nunchaku` in my current installation).

Best regards,
ioannis