Support diamond inheritance in TLA+ modules #74

TLA+ has a really rare scoping rule where including the exact same operator more than once is ok and does nothing. We currently would flag this as an error even though it should work in principle.

Example:

• module A declares operator foo
• module B extends module A
• module C extends module A
• module D extends modules B and C

D gets one unique copy of operator foo. As it is now, PGo would complain about a redefinition of foo.