Also improve type inference of Relations.tla for TLA2B

src/main/resources/de/tlc4b/standardModules/FunctionsAsRelations.tla

 ------------------------ MODULE FunctionsAsRelations ----------------------------------
 EXTENDS FiniteSets, Functions, TLC, Sequences
 
-LOCAL RelDom(f) == { <<x[1], x[2]>>[1] : x \in f } \* The domain of the function, syntax is weird to help TLA2B typechecker
-LOCAL RelRan(f) == { <<x[1], x[2]>>[2] : x \in f } \* The range of the function, syntax is weird to help TLA2B typechecker
+LOCAL GetKey(x) == <<x[1], x[2]>>[1] \* Get key of relational pair, also used as a type hint for TLA2B
+
+LOCAL RelDom(f) == {GetKey(x): x \in f} \* The domain of the function
+LOCAL RelRan(f) == {x[2]: x \in f} \* The range of the function
 LOCAL MakeRel(f) == {<<x, f[x]>>: x \in DOMAIN f} 
  \* Converting a TLA+ function to a set of pairs
 LOCAL Rel(S, T) == SUBSET (S \times T) \* The set of relations

src/main/resources/de/tlc4b/standardModules/Relations.tla

 ---------------------------- MODULE Relations ----------------------------
 EXTENDS FiniteSets, Naturals, Sequences, TLC
 
+LOCAL GetKey(x) == <<x[1], x[2]>>[1] \* Get key of relational pair, also used as a type hint for TLA2B
+
 Relations(S, T) == SUBSET (S \times T)
  \* The set of all relations
  
-RelDomain(R) == {x[1]: x \in R}
+RelDomain(R) == {GetKey(x): x \in R}
   \* The domain of the relation R
 
 RelRange(R) == {x[2]: x \in R}
@@ -13,10 +15,10 @@ RelRange(R) == {x[2]: x \in R}
 RelId(S) == {<<x,x>>: x \in S}
  \* The identity relation of set S
 
-RelDomRes(S, R) == {x \in R: x[1] \in S} 
+RelDomRes(S, R) == {x \in R: GetKey(x) \in S}
  \* The restriction on the domain of R for set S
  
-RelDomSub(S, R) == {x \in R: x[1] \notin S} 
+RelDomSub(S, R) == {x \in R: GetKey(x) \notin S}
  \* The subtraction on the domain of R for set S
 
 RelRanRes(R, S) == {x \in R: x[2] \in S}