diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index c8595a335e210ca306e0fb9d24c16b7bff5b208a..589cf83c0837a13d9e9f54a4794000c96a85aef2 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -1367,8 +1367,13 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
 			throw new TypeErrorException("Excepted '" + expected + "' , found "
 					+ found + "'");
 		}
-		setType(node.getExpression(), new SetType(new UntypedType()));
+		
+		setType(node.getExpression(), new UntypedType());
 		node.getExpression().apply(this);
+		BType type = getType(node.getExpression());
+		if (! (type instanceof FunctionType)){
+			new SetType(new UntypedType()).unify(type, this);
+		}
 	}
 
 	@Override
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index f07ed67e7e8aca5c7b609bb7a538a4fd3707bdd9..8f9eff5e0e2d5cfedeb33f5b2b01878949b473a7 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -920,7 +920,12 @@ public class TLAPrinter extends DepthFirstAdapter {
 			tlaModuleString.append(" : ");
 		}
 
-		node.getPredicate().apply(this);
+		if (typeRestrictor.isARemovedNode(node.getPredicate())) {
+			tlaModuleString.append("TRUE");
+		} else {
+			node.getPredicate().apply(this);
+		}
+		
 		tlaModuleString.append(" /\\ ");
 		node.getSubstitution().apply(this);
 		printUnchangedVariables(node, true);
@@ -2050,11 +2055,16 @@ public class TLAPrinter extends DepthFirstAdapter {
 
 	@Override
 	public void caseACardExpression(ACardExpression node) {
-		inACardExpression(node);
-		tlaModuleString.append("Cardinality(");
-		node.getExpression().apply(this);
-		tlaModuleString.append(")");
-		outACardExpression(node);
+		BType type = typechecker.getType(node.getExpression());
+		if(type instanceof FunctionType){
+			tlaModuleString.append("Cardinality(DOMAIN(");
+			node.getExpression().apply(this);
+			tlaModuleString.append("))");
+		}else{
+			tlaModuleString.append("Cardinality(");
+			node.getExpression().apply(this);
+			tlaModuleString.append(")");	
+		}
 	}
 
 	@Override
diff --git a/src/test/java/de/tlc4b/util/TLC4BTester.java b/src/test/java/de/tlc4b/util/TLC4BTester.java
index 651c0e5c249d54e8d92917a10739c159c017ae03..438b8c00fb31fc1c39cc14434fa57270b86b0dc7 100644
--- a/src/test/java/de/tlc4b/util/TLC4BTester.java
+++ b/src/test/java/de/tlc4b/util/TLC4BTester.java
@@ -7,7 +7,7 @@ public class TLC4BTester {
 
 	public static void main(String[] args) throws Exception {
 		System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
-		TLC4B.test(args,false);
+		TLC4B.test(args,true);
 	}
 
 }
diff --git a/src/test/resources/basics/SubstitutionsTest.mch b/src/test/resources/basics/SubstitutionsTest.mch
index 17c44c404d79cd73dad86e3e2435f880b17a6052..6703ea100127ecb59890c04cd716f69e4bda9bf1 100644
--- a/src/test/resources/basics/SubstitutionsTest.mch
+++ b/src/test/resources/basics/SubstitutionsTest.mch
@@ -6,5 +6,7 @@ OPERATIONS
 op1 = PRE 1 = 1 THEN x := 2 END;
 op2 = LET a, b, c BE a = 1 & b : {1} & c = 2 IN x := 2 END;
 op3 = SELECT 1=1 THEN x := 1 WHEN 1=1 THEN x:=2 ELSE x:= 3 END;
-op4 = SELECT 1=1 THEN x := 1 WHEN 1=1 THEN x:=2 WHEN 1=1 THEN x:=3 ELSE x:= 4 END
+op4 = SELECT 1=1 THEN x := 1 WHEN 1=1 THEN x:=2 WHEN 1=1 THEN x:=3 ELSE x:= 4 END;
+
+op5 = BEGIN LET p BE p = 2 IN x:= p END END
 END
\ No newline at end of file