diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index 01baa17b896614ef4e2373e41687de9a4ad11b50..55e34f707b6f8ae63d3d45fb9fd816a389ec50a6 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -412,13 +412,24 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
 		
 		UntypedType x = new UntypedType();
 		setType(node.getThen(), x);
+		node.getElsifs().forEach(n -> setType(n, x));
 		setType(node.getElse(), x);
 		node.getThen().apply(this);
+		node.getElsifs().forEach(n -> n.apply(this));
 		node.getElse().apply(this);
 		BType found = getType(node.getThen());
 		unify(getType(node), found, node);
 	}
 
+	@Override
+	public void caseAIfElsifExprExpression(AIfElsifExprExpression node) {
+		setType(node.getCondition(), BoolType.getInstance());
+		node.getCondition().apply(this);
+
+		setType(node.getThen(), getType(node));
+		node.getThen().apply(this);
+	}
+
 	@Override
 	public void caseANotEqualPredicate(ANotEqualPredicate node) {
 		try {
diff --git a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
index 31727e952f81872cc5877d164b02ca5ec00f79dc..207a6ad2b6372714b019d6be54704386c971ea5d 100644
--- a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
+++ b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
@@ -33,7 +33,7 @@ public class UnsupportedConstructsFinder extends DepthFirstAdapter {
 		add(AFloatSetExpression.class);
 		add(ARealExpression.class);
 
-		add(AIfElsifExprExpression.class);
+		// should have been rewritten in parser
 		add(AIfPredicatePredicate.class);
 		add(AIfElsifPredicatePredicate.class);
 
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index b43f7a120d8d5a01f9d2dda0b1119daab672ecc5..aa0c57c918bff4b949a8bc77eafcd0babf7679ab 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -1146,13 +1146,34 @@ public class TLAPrinter extends DepthFirstAdapter {
 	
 	@Override
 	public void caseAIfThenElseExpression(AIfThenElseExpression node) {
-		moduleStringAppend("(IF ");
+		if (node.getElsifs().isEmpty()) {
+			moduleStringAppend("(IF ");
+			node.getCondition().apply(this);
+			moduleStringAppend(" THEN ");
+			node.getThen().apply(this);
+			moduleStringAppend(" ELSE ");
+			node.getElse().apply(this);
+			moduleStringAppend(")");
+		} else {
+			moduleStringAppend("(CASE ");
+			node.getCondition().apply(this);
+			moduleStringAppend(" -> ");
+			node.getThen().apply(this);
+			node.getElsifs().forEach(n -> {
+				moduleStringAppend(" [] ");
+				n.apply(this);
+			});
+			moduleStringAppend(" [] OTHER -> ");
+			node.getElse().apply(this);
+			moduleStringAppend(")");
+		}
+	}
+
+	@Override
+	public void caseAIfElsifExprExpression(AIfElsifExprExpression node) {
 		node.getCondition().apply(this);
-		moduleStringAppend(" THEN ");
+		moduleStringAppend(" -> ");
 		node.getThen().apply(this);
-		moduleStringAppend(" ELSE ");
-		node.getElse().apply(this);
-		moduleStringAppend(")");
 	}
 
 	@Override