Align SequenceExtTheorems with SequenceExtTheorems_proofs

lemmy · lemmy · commit c5eed5991795 · 2020-02-27T12:45:35.000-08:00
diff --git a/modules/SequenceExtTheorems.tla b/modules/SequenceExtTheorems.tla
@@ -7,7 +7,7 @@ LEMMA AppendTransitivityIsInjective
      == ASSUME NEW S, NEW seq \in Seq(S),
                IsInjective(seq),
                NEW elt \in S,
-               elt \notin { seq[x]: x \in DOMAIN seq }
+               elt \notin Range(seq)
         PROVE IsInjective(Append(seq, elt))
 
 LEMMA TailTransitivityIsInjective
