Here's a little more detail to explain Stephan's response. TLC has a mechanism for replacing a definition in a module with Java methods that TLC uses to evaluate expressions containing the defined operator. This mechanism is used for the definition of Seq in the standard Sequences module. It allows TLC to evaluate an _expression_ like <<-42>> \in Seq(Nat) even though TLC can't evaluate Seq(Nat). In the Sequences module, Seq is defined in terms of Nat. However, because TLC does not use that definition in evaluating expressions containing Seq, overriding the definition of Nat does not change how TLC evaluates expressions containing Seq.