diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index d2e98a2..02373e7 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -20,22 +20,6 @@ jobs:
     - name: Get current date
       id: date
       run: echo "::set-output name=date::$(date +'%Y%m%d%H%M')"
-    # Do not download and install TLAPS over and over again.
-    - uses: actions/cache@v1
-      id: cache
-      with:
-        path: tlaps/
-        key: tlaps1.4.5
-    - name: Get TLAPS
-      if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above
-      run: wget https://tla.msr-inria.inria.fr/tlaps/dist/current/tlaps-1.4.5-x86_64-linux-gnu-inst.bin
-    - name: Install TLAPS
-      if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above
-      run: |
-        chmod +x tlaps-1.4.5-x86_64-linux-gnu-inst.bin
-        ./tlaps-1.4.5-x86_64-linux-gnu-inst.bin -d tlaps
-    - name: Run TLAPS
-      run: tlaps/bin/tlapm --cleanfp -I tlaps/ -I modules/ modules/SequencesExtTheorems_proofs.tla
     - name: Build with Ant
       run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}}
     - name: Copied CommunityModules-SomeDate.jar to CommunityModules.jar
diff --git a/modules/Functions.tla b/modules/Functions.tla
index a96195a..38ee6f1 100644
--- a/modules/Functions.tla
+++ b/modules/Functions.tla
@@ -27,10 +27,18 @@ Inverse(f,S,T) == [t \in T |-> CHOOSE s \in S : t \in Range(f) => f[s] = t]
 
 
 (***************************************************************************)
-(* A map is an injection iff each element in the domain maps to a distinct *)
-(* element in the range.                                                   *)
+(* A function is injective iff it maps each element in its domain to a     *)
+(* distinct element.                                                       *)
+(*                                                                         *)
+(* This definition is overridden by TLC in the Java class SequencesExt.    *)
+(* The operator is overridden by the Java method with the same name.       *)
 (***************************************************************************)
-Injection(S,T) == { M \in [S -> T] : \A a,b \in S : M[a] = M[b] => a = b }
+IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b
+
+(***************************************************************************)
+(* Set of injections between two sets.                                     *)
+(***************************************************************************)
+Injection(S,T) == { M \in [S -> T] : IsInjective(M) }
 
 
 (***************************************************************************)
@@ -57,7 +65,7 @@ ExistsBijection(S,T)  == Bijection(S,T) # {}
 
 =============================================================================
 \* Modification History
-\* Last modified Wed Jul 10 20:32:37 CEST 2013 by merz
+\* Last modified Sun Dec 27 09:38:06 CET 2020 by merz
 \* Last modified Wed Jun 05 12:14:19 CEST 2013 by bhargav
 \* Last modified Fri May 03 12:55:35 PDT 2013 by tomr
 \* Created Thu Apr 11 10:30:48 PDT 2013 by tomr
diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla
index 80ee88f..73d802d 100644
--- a/modules/SequencesExt.tla
+++ b/modules/SequencesExt.tla
@@ -18,19 +18,6 @@ ToSet(s) ==
   (*************************************************************************)
   { s[i] : i \in DOMAIN s }
 
-IsInjective(s) == 
-  (*************************************************************************)
-  (* TRUE iff the sequence s contains no duplicates where two elements     *)
-  (* a, b of s are defined to be duplicates iff a = b.  In other words,    *)
-  (* Cardinality(ToSet(s)) = Len(s)                                        *)
-  (*                                                                       *)
-  (* This definition is overridden by TLC in the Java class SequencesExt.  *)
-  (* The operator is overridden by the Java method with the same name.     *)
-  (*                                                                       *)
-  (* Also see Functions!Injective operator.                                *)
-  (*************************************************************************)
-  \A i, j \in DOMAIN s: (s[i] = s[j]) => (i = j)
-
 SetToSeq(S) == 
   (**************************************************************************)
   (* Convert a set to some sequence that contains all the elements of the   *)
@@ -121,6 +108,12 @@ RemoveAt(s, i) ==
 
 -----------------------------------------------------------------------------
 
+Cons(elt, seq) == 
+    (***************************************************************************)
+    (* Cons prepends an element at the beginning of a sequence.                *)
+    (***************************************************************************)
+    <<elt>> \o seq
+
 Front(s) == 
   (**************************************************************************)
   (* The sequence formed by removing its last element.                      *)
diff --git a/modules/SequencesExtTheorems.tla b/modules/SequencesExtTheorems.tla
deleted file mode 100644
index e1c00f3..0000000
--- a/modules/SequencesExtTheorems.tla
+++ /dev/null
@@ -1,27 +0,0 @@
------------------------- MODULE SequencesExtTheorems ------------------------
-LOCAL INSTANCE SequencesExt
-LOCAL INSTANCE Sequences
-LOCAL INSTANCE Functions
-
-LEMMA AppendTransitivityIsInjective
-     == ASSUME NEW S, NEW seq \in Seq(S),
-               IsInjective(seq),
-               NEW elt \in S,
-               elt \notin Range(seq)
-        PROVE IsInjective(Append(seq, elt))
-
-LEMMA TailTransitivityIsInjective
-     == ASSUME NEW S, NEW seq \in Seq(S),
-               seq # <<>>,
-               IsInjective(seq)
-        PROVE IsInjective(Tail(seq))
-
-LEMMA HeadTailRange ==
-  ASSUME NEW S, NEW seq \in Seq(S), seq # << >>, IsInjective(seq)
-  PROVE  /\ Head(seq) \in Range(seq)
-         /\ Range(Tail(seq)) = Range(seq) \ {Head(seq)}
-
-=============================================================================
-\* Modification History
-\* Last modified Thu Feb 27 11:38:41 PST 2020 by markus
-\* Created Tue Feb 25 20:49:08 PST 2020 by markus
diff --git a/modules/SequencesExtTheorems_proofs.tla b/modules/SequencesExtTheorems_proofs.tla
deleted file mode 100644
index fa7a700..0000000
--- a/modules/SequencesExtTheorems_proofs.tla
+++ /dev/null
@@ -1,71 +0,0 @@
---------------------- MODULE SequencesExtTheorems_proofs ---------------------
-LOCAL INSTANCE SequencesExt
-LOCAL INSTANCE Sequences
-LOCAL INSTANCE Naturals
-LOCAL INSTANCE Functions
-LOCAL INSTANCE TLAPS
-
-LEMMA AppendTransitivityIsInjective \* With TLAPS 1.4.4+ (3ed0cde)
-     == ASSUME NEW S, NEW seq \in Seq(S),
-               IsInjective(seq),
-               NEW elt \in S,
-               elt \notin Range(seq)
-        PROVE IsInjective(Append(seq, elt))
-BY DEF IsInjective, Range
-
-LEMMA TailTransitivityIsInjective \* With TLAPS 1.4.3
-     == ASSUME NEW S, NEW seq \in Seq(S),
-               seq # <<>>,
-               IsInjective(seq)
-        PROVE IsInjective(Tail(seq))
-  <1> DEFINE ts == Tail(seq)
-  <1>1. IsInjective(ts) 
-    <2> SUFFICES ASSUME NEW i \in DOMAIN ts, NEW j \in DOMAIN ts,
-                        ts[i] = ts[j]
-                 PROVE  i = j
-      BY DEF IsInjective
-    <2>1. ts[i] = seq[i + 1] /\ ts[j] = seq[j + 1] 
-      BY SMT
-    <2>2. 1..Len(ts) = 1..Len(seq)-1
-      BY SMT
-    <2>3. 1..Len(ts) \subseteq 1..Len(seq)
-      BY SMT
-    <2>4. DOMAIN ts = 1..Len(seq)-1
-      BY SMT
-    <2>5. DOMAIN seq = 1..Len(seq)
-      BY SMT
-    <2>6. \A r, s \in 1..Len(seq): (seq[r] = seq[s]) => (r = s)
-      BY Isa, <2>5 DEF IsInjective
-    <2>7. seq \in [1..Len(seq) -> Range(seq)]
-      BY Isa, <2>5 DEF Range
-    <2>8. DOMAIN ts \subseteq DOMAIN seq
-      BY Isa, <2>2, <2>3, <2>4, <2>7
-    <2>9. QED BY <2>1, <2>2, <2>3, <2>5, <2>6, <2>7, <2>8 DEF IsInjective
-  <1>2. QED BY <1>1
-
-LEMMA HeadTailRange == \* With TLAPS 1.4.5 (but not 1.4.3)
-  ASSUME NEW S, NEW seq \in Seq(S), seq # << >>, IsInjective(seq)
-  PROVE  /\ Head(seq) \in Range(seq)
-         /\ Range(Tail(seq)) = Range(seq) \ {Head(seq)}
-<1>1. Head(seq) \in Range(seq)
-  BY SMT DEF Range
-<1>2. Range(Tail(seq)) \subseteq Range(seq)
-  BY SMT DEF Range
-<1>3. Head(seq) \notin Range(Tail(seq))
-  BY SMT DEF Range, IsInjective
-<1>4. ASSUME NEW x \in Range(seq), x # Head(seq)
-      PROVE  x \in Range(Tail(seq))
-  <2>1. PICK i \in DOMAIN seq : x = seq[i]
-    BY Isa DEF Range
-  <2>2. i # 1
-    BY SMT, <2>1, <1>4
-  <2>3. /\ i-1 \in DOMAIN Tail(seq)
-        /\ x = Tail(seq)[i-1]
-    BY SMT, <2>1, <2>2
-  <2>. QED  BY Isa, <2>3 DEF Range
-<1>. QED  BY Isa, <1>1, <1>2, <1>3, <1>4
-
-=============================================================================
-\* Modification History
-\* Last modified Thu Feb 27 11:44:49 PST 2020 by markus
-\* Created Thu Feb 27 11:27:48 PST 2020 by markus
diff --git a/modules/tlc2/overrides/Functions.java b/modules/tlc2/overrides/Functions.java
new file mode 100644
index 0000000..2cd3440
--- /dev/null
+++ b/modules/tlc2/overrides/Functions.java
@@ -0,0 +1,83 @@
+/*******************************************************************************
+ * Copyright (c) 2019 Microsoft Research. All rights reserved. 
+ *
+ * The MIT License (MIT)
+ * 
+ * Permission is hereby granted, free of charge, to any person obtaining a copy 
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software. 
+ * 
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+package tlc2.overrides;
+
+import java.util.Arrays;
+
+import tlc2.output.EC;
+import tlc2.tool.EvalException;
+import tlc2.value.Values;
+import tlc2.value.impl.BoolValue;
+import tlc2.value.impl.SetEnumValue;
+import tlc2.value.impl.TupleValue;
+import tlc2.value.impl.Value;
+
+public final class Functions {
+	
+	private Functions() {
+		// no-instantiation!
+	}
+	
+	@TLAPlusOperator(identifier = "IsInjective", module = "Functions", warn = false)
+	public static BoolValue IsInjective(final Value val) {
+		if (val instanceof TupleValue) {
+			return isInjectiveNonDestructive(((TupleValue) val).elems);
+		} else {
+			final Value conv = val.toTuple();
+			if (conv == null) {
+				throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
+						new String[] { "IsInjective", "sequence", Values.ppr(val.toString()) });
+			}
+			return isInjectiveDestructive(((TupleValue) conv).elems);
+		}
+	}
+	
+	// O(n log n) runtime and O(1) space.
+	private static BoolValue isInjectiveDestructive(final Value[] values) {
+		Arrays.sort(values);
+		for (int i = 1; i < values.length; i++) {
+			if (values[i-1].equals(values[i])) {
+				return BoolValue.ValFalse;
+			}
+		}
+		return BoolValue.ValTrue;
+	}
+
+	// Assume small arrays s.t. the naive approach with O(n^2) runtime but O(1)
+	// space is good enough. Sorting values in-place is a no-go because it
+	// would modify the TLA+ tuple. Elements can be any sub-type of Value, not
+	// just IntValue.
+	private static BoolValue isInjectiveNonDestructive(final Value[] values) {
+		for (int i = 0; i < values.length; i++) {
+			for (int j = i + 1; j < values.length; j++) {
+				if (values[i].equals(values[j])) {
+					return BoolValue.ValFalse;
+				}
+			}
+		}
+		return BoolValue.ValTrue;
+	}
+}
diff --git a/modules/tlc2/overrides/SequencesExt.java b/modules/tlc2/overrides/SequencesExt.java
index a1d3c3d..f9bdf65 100644
--- a/modules/tlc2/overrides/SequencesExt.java
+++ b/modules/tlc2/overrides/SequencesExt.java
@@ -24,7 +24,6 @@
  * Contributors:
  *   Markus Alexander Kuppe - initial API and implementation
  ******************************************************************************/
-import java.util.Arrays;
 
 import tlc2.output.EC;
 import tlc2.tool.EvalException;
@@ -40,46 +39,6 @@ private SequencesExt() {
 		// no-instantiation!
 	}
 	
-	@TLAPlusOperator(identifier = "IsInjective", module = "SequencesExt", warn = false)
-	public static BoolValue IsInjective(final Value val) {
-		if (val instanceof TupleValue) {
-			return isInjectiveNonDestructive(((TupleValue) val).elems);
-		} else {
-			final Value conv = val.toTuple();
-			if (conv == null) {
-				throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
-						new String[] { "IsInjective", "sequence", Values.ppr(val.toString()) });
-			}
-			return isInjectiveDestructive(((TupleValue) conv).elems);
-		}
-	}
-	
-	// O(n log n) runtime and O(1) space.
-	private static BoolValue isInjectiveDestructive(final Value[] values) {
-		Arrays.sort(values);
-		for (int i = 1; i < values.length; i++) {
-			if (values[i-1].equals(values[i])) {
-				return BoolValue.ValFalse;
-			}
-		}
-		return BoolValue.ValTrue;
-	}
-
-	// Assume small arrays s.t. the naive approach with O(n^2) runtime but O(1)
-	// space is good enough. Sorting values in-place is a no-go because it
-	// would modify the TLA+ tuple. Elements can be any sub-type of Value, not
-	// just IntValue.
-	private static BoolValue isInjectiveNonDestructive(final Value[] values) {
-		for (int i = 0; i < values.length; i++) {
-			for (int j = i + 1; j < values.length; j++) {
-				if (values[i].equals(values[j])) {
-					return BoolValue.ValFalse;
-				}
-			}
-		}
-		return BoolValue.ValTrue;
-	}
-	
 	/*
 	 * Improve carbon footprint of SequencesExt!SetToSeq. Convert SetEnumValue to
 	 * TupleValue (linear in the number of elements) instead of generating the set
diff --git a/modules/tlc2/overrides/TLCOverrides.java b/modules/tlc2/overrides/TLCOverrides.java
index 1881eca..d1a3b57 100644
--- a/modules/tlc2/overrides/TLCOverrides.java
+++ b/modules/tlc2/overrides/TLCOverrides.java
@@ -34,12 +34,12 @@ public class TLCOverrides implements ITLCOverrides {
 	public Class[] get() {
 		try {
 			Json.resolves();
-			return new Class[] { TLCExt.class, IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class, FiniteSetsExt.class };
+			return new Class[] { TLCExt.class, IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class, FiniteSetsExt.class, Functions.class };
 		} catch (NoClassDefFoundError e) {
 			System.out.println(
 					"com.fasterxml.jackson dependencies of Json overrides not found, Json module won't work unless "
 					+ "the libraries in the lib/ folder of the CommunityModules have been added to the classpath of TLC.");
 		}
-		return new Class[] { TLCExt.class, IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class, FiniteSetsExt.class };
+		return new Class[] { TLCExt.class, IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class, FiniteSetsExt.class, Functions.class };
 	}
 }
diff --git a/tests/AllTests.tla b/tests/AllTests.tla
index 990fdf6..0cc948c 100644
--- a/tests/AllTests.tla
+++ b/tests/AllTests.tla
@@ -9,6 +9,7 @@ EXTENDS SequencesExtTests,
         JsonTests,
         BitwiseTests,
         IOUtilsTests,
-        FiniteSetsExtTests
+        FiniteSetsExtTests,
+        FunctionsTests
 
 ===========================================
\ No newline at end of file
diff --git a/tests/FunctionsTests.tla b/tests/FunctionsTests.tla
new file mode 100644
index 0000000..4ba4f1d
--- /dev/null
+++ b/tests/FunctionsTests.tla
@@ -0,0 +1,19 @@
+------------------------- MODULE FunctionsTests -------------------------
+EXTENDS Functions, Naturals, TLC, TLCExt, FiniteSets
+
+ASSUME(IsInjective(<<>>))
+ASSUME(IsInjective(<<1>>))
+ASSUME(IsInjective(<<1,2,3>>))
+ASSUME(~IsInjective(<<1,1>>))
+ASSUME(~IsInjective(<<1,1,2,3>>))
+
+ASSUME(IsInjective([i \in 1..10 |-> i]))
+ASSUME(IsInjective([i \in 1..10 |-> {i}]))
+ASSUME(IsInjective([i \in 1..10 |-> {i}]))
+ASSUME(~IsInjective([i \in 1..10 |-> {1,2,3}]))
+
+ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n{}", IsInjective({})))
+ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n[a: 1, b: 2]", IsInjective([a: 1, b: 2])))
+ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n(0 :> 0 @@ 1 :> 1 @@ 2 :> 2)", IsInjective([i \in 0..2 |-> i])))
+
+=============================================================================
diff --git a/tests/SequencesExtTests.tla b/tests/SequencesExtTests.tla
index ffe1007..e8cd028 100644
--- a/tests/SequencesExtTests.tla
+++ b/tests/SequencesExtTests.tla
@@ -10,21 +10,6 @@ ASSUME(ToSet([i \in 1..10 |-> i]) = 1..10)
 ASSUME(ToSet(Tail([i \in 1..10 |-> i])) = 2..10)
 ASSUME(ToSet([i \in 0..9 |-> 42]) = {42})
 
-ASSUME(IsInjective(<<>>))
-ASSUME(IsInjective(<<1>>))
-ASSUME(IsInjective(<<1,2,3>>))
-ASSUME(~IsInjective(<<1,1>>))
-ASSUME(~IsInjective(<<1,1,2,3>>))
-
-ASSUME(IsInjective([i \in 1..10 |-> i]))
-ASSUME(IsInjective([i \in 1..10 |-> {i}]))
-ASSUME(IsInjective([i \in 1..10 |-> {i}]))
-ASSUME(~IsInjective([i \in 1..10 |-> {1,2,3}]))
-
-ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n{}", IsInjective({})))
-ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n[a: 1, b: 2]", IsInjective([a: 1, b: 2])))
-ASSUME(AssertError("The argument of IsInjective should be a sequence, but instead it is:\n(0 :> 0 @@ 1 :> 1 @@ 2 :> 2)", IsInjective([i \in 0..2 |-> i])))
-
 ASSUME(SetToSeq({}) = <<>>)
 ASSUME(SetToSeq({1}) = <<1>>)
 ASSUME(LET s == {"t","l","a","p","l","u","s"}