diff --git a/base/src/main/java/org/arend/typechecking/error/local/IdpPatternError.java b/base/src/main/java/org/arend/typechecking/error/local/IdpPatternError.java
index 7d008f90c..36908131d 100644
--- a/base/src/main/java/org/arend/typechecking/error/local/IdpPatternError.java
+++ b/base/src/main/java/org/arend/typechecking/error/local/IdpPatternError.java
@@ -37,7 +37,7 @@ public static String subst(String substVar, String paramVar, String freeVar) {
   }
 
   public static String noParameter() {
-    return "One of the sides in the expected type should be a variable";
+    return "One of the sides in the expected type should be a parameter";
   }
 
   @Override
diff --git a/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java b/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java
index 4c37005a3..a7040bc9a 100644
--- a/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java
+++ b/base/src/main/java/org/arend/typechecking/visitor/CheckTypeVisitor.java
@@ -4016,11 +4016,8 @@ public TypecheckingResult visitCase(Concrete.CaseExpression expr, Expression exp
         list.append(link);
         if (caseArg.isElim) {
           if (argTypeExpr != null) {
-            Expression actualArgType = exprResult.type.subst(substitution);
-            if (!CompareVisitor.compare(myEquations, CMP.EQ, actualArgType, argTypeExpr, Type.OMEGA, caseArg.type)) {
-              errorReporter.report(new TypeMismatchError(actualArgType, argTypeExpr, caseArg.expression));
-              return null;
-            }
+            errorReporter.report(new TypecheckingError("Explicit type annotation is not allowed with \\elim", caseArg.expression));
+            return null;
           }
           Binding origBinding = ((ReferenceExpression) exprResult.expression).getBinding();
           origElimBindings.put(asRef, origBinding);
diff --git a/src/test/java/org/arend/typechecking/constructions/ArrayTest.java b/src/test/java/org/arend/typechecking/constructions/ArrayTest.java
index a7a2701d7..d9a19ab41 100644
--- a/src/test/java/org/arend/typechecking/constructions/ArrayTest.java
+++ b/src/test/java/org/arend/typechecking/constructions/ArrayTest.java
@@ -425,7 +425,7 @@ public void casePatternMatchingTest5() {
   public void casePatternMatchingTest6() {
     typeCheckModule("""
       \\func test {A : \\Set} {n : Nat} (l : Array A n) : Nat
-        => \\case \\elim n, \\elim l : Array A n \\with {
+        => \\case \\elim n, l : Array A n \\with {
           | 0, nil => 0
           | suc n, a :: l => 1
         }
diff --git a/src/test/java/org/arend/typechecking/constructions/CaseTest.java b/src/test/java/org/arend/typechecking/constructions/CaseTest.java
index d6aaaec84..5500c8966 100644
--- a/src/test/java/org/arend/typechecking/constructions/CaseTest.java
+++ b/src/test/java/org/arend/typechecking/constructions/CaseTest.java
@@ -27,144 +27,157 @@ public void testCase() {
 
   @Test
   public void testCaseReturn() {
-    typeCheckModule(
-      "\\data Bool | true | false\n" +
-      "\\func not (b : Bool) => \\case b \\return Bool \\with { | true => false | false => true }\n" +
-      "\\func f (b : Bool) => \\case b \\as x \\return not (not x) = x \\with { | true => idp | false => idp }");
+    typeCheckModule("""
+      \\data Bool | true | false
+      \\func not (b : Bool) => \\case b \\return Bool \\with { | true => false | false => true }
+      \\func f (b : Bool) => \\case b \\as x \\return not (not x) = x \\with { | true => idp | false => idp }
+      """);
   }
 
   @Test
   public void testCaseReturnError() {
-    typeCheckModule(
-      "\\data Bool | true | false\n" +
-      "\\func not (b : Bool) => \\case b \\return Bool \\with { | true => false | false => true }\n" +
-      "\\func f (b : Bool) => \\case b \\return not (not b) = b \\with { | true => idp | false => idp }", 2);
+    typeCheckModule("""
+      \\data Bool | true | false
+      \\func not (b : Bool) => \\case b \\return Bool \\with { | true => false | false => true }
+      \\func f (b : Bool) => \\case b \\return not (not b) = b \\with { | true => idp | false => idp }
+      """, 2);
     assertThatErrorsAre(Matchers.error(), Matchers.error());
   }
 
   @Test
   public void testCaseArguments() {
-    typeCheckModule(
-      "\\data Bool | true | false\n" +
-      "\\func not (b : Bool) => \\case b \\return Bool \\with { | true => false | false => true }\n" +
-      "\\data Or (A B : \\Type) | inl A | inr B\n" +
-      "\\func f (b : Bool) : (b = true) `Or` (b = false) => \\case b \\as x, idp : b = x \\with { | true, p => inl p | false, p => inr p }");
+    typeCheckModule("""
+      \\data Bool | true | false
+      \\func not (b : Bool) => \\case b \\return Bool \\with { | true => false | false => true }
+      \\data Or (A B : \\Type) | inl A | inr B
+      \\func f (b : Bool) : (b = true) `Or` (b = false) => \\case b \\as x, idp : b = x \\with { | true, p => inl p | false, p => inr p }
+      """);
   }
 
   @Test
   public void testCaseMultipleArguments() {
-    typeCheckModule(
-      "\\func \\infix 4 < (n m : Nat) => Nat\n" +
-      "\\func f1 (n k : Nat) : Nat => \\case k \\as z, n < z \\as r, idp : r = n < z \\with { | k, T, P => 0 }\n" +
-      "\\func f2 (n k : Nat) (p : n < k) : Nat => \\case k \\as z, p \\as r : n < z, idp : r = {n < z} p \\with { | k, p, s => 0 }\n" +
-      "\\func f3 (n k : Nat) (p : n < k) : Nat => \\case k \\as z, p \\as r : n < z, idp : r = {n < k} p \\with { | k, p, s => 0 }");
+    typeCheckModule("""
+      \\func \\infix 4 < (n m : Nat) => Nat
+      \\func f1 (n k : Nat) : Nat => \\case k \\as z, n < z \\as r, idp : r = n < z \\with { | k, T, P => 0 }
+      \\func f2 (n k : Nat) (p : n < k) : Nat => \\case k \\as z, p \\as r : n < z, idp : r = {n < z} p \\with { | k, p, s => 0 }
+      \\func f3 (n k : Nat) (p : n < k) : Nat => \\case k \\as z, p \\as r : n < z, idp : r = {n < k} p \\with { | k, p, s => 0 }
+      """);
   }
 
   @Test
   public void caseElimResolveError() {
-    resolveNamesDef(
-      "\\func f (x : Nat) : Nat => \\case \\elim x \\with {\n" +
-      "  | _ => x\n" +
-      "}", 1);
+    resolveNamesDef("""
+      \\func f (x : Nat) : Nat => \\case \\elim x \\with {
+        | _ => x
+      }""", 1);
     assertThatErrorsAre(notInScope("x"));
   }
 
   @Test
   public void caseElim() {
-    typeCheckDef(
-      "\\func f (x : Nat) (p : x = 0) => \\case \\elim x, p : x = 0 \\return x = 0 \\with {\n" +
-      "  | 0, _ => idp\n" +
-      "  | suc _, p => p\n" +
-      "}");
+    typeCheckDef("""
+      \\func f (x : Nat) (p : x = 0) => \\case \\elim x, p : x = 0 \\return x = 0 \\with {
+        | 0, _ => idp
+        | suc _, p => p
+      }
+      """);
   }
 
   @Test
   public void caseElimSubst() {
-    typeCheckDef(
-      "\\func f (x : Nat) (p : x = 0) : x = 0 => \\case \\elim x, p \\with {\n" +
-      "  | 0, _ => idp\n" +
-      "  | suc _, p => p\n" +
-      "}");
+    typeCheckDef("""
+      \\func f (x : Nat) (p : x = 0) : x = 0 => \\case \\elim x, p \\with {
+        | 0, _ => idp
+        | suc _, p => p
+      }
+      """);
   }
 
   @Test
   public void caseElimSubstType() {
-    typeCheckDef(
-      "\\func f (x : Nat) (p : x = 0) : x = 0 => \\case \\elim x, \\elim p : x = 0 \\with {\n" +
-      "  | 0, _ => idp\n" +
-      "  | suc _, p => p\n" +
-      "}");
+    typeCheckDef("""
+      \\func f (x : Nat) (p : x = 0) : x = 0 => \\case \\elim x, p : x = 0 \\with {
+        | 0, _ => idp
+        | suc _, p => p
+      }
+      """);
   }
 
   @Test
   public void caseElimTypeError() {
-    typeCheckDef(
-      "\\func f (x : \\Set0) => \\case \\elim x : \\Set1 \\return Nat \\with {\n" +
-      "  | _ => 0\n" +
-      "}", 1);
-    assertThatErrorsAre(typeMismatchError());
+    typeCheckDef("""
+      \\func f (x : \\Set0) => \\case \\elim x : \\Set1 \\return Nat \\with {
+        | _ => 0
+      }
+      """, 1);
   }
 
   @Test
   public void checkElimTypeTest() {
-    typeCheckModule(
-      "\\func test (A : \\Type) (x : A) (p : x = x) : p = p =>\n" +
-      "  \\case \\elim x, \\elim p \\with {\n" +
-      "    | _, _ => idp\n" +
-      "  }");
+    typeCheckModule("""
+      \\func test (A : \\Type) (x : A) (p : x = x) : p = p =>
+        \\case \\elim x, \\elim p \\with {
+          | _, _ => idp
+        }
+      """);
   }
 
   @Test
   public void checkElimTypeError() {
-    typeCheckModule(
-      "\\func test (A : \\Type) (x : A) (p : x = x) : p = p =>\n" +
-      "  \\case \\elim x \\with {\n" +
-      "    | _ => {?}\n" +
-      "  }", 2);
+    typeCheckModule("""
+      \\func test (A : \\Type) (x : A) (p : x = x) : p = p =>
+        \\case \\elim x \\with {
+          | _ => {?}
+        }
+      """, 2);
     assertThatErrorsAre(elimSubstError("p"), goal(2));
   }
 
   @Test
   public void checkElimTypeError2() {
-    typeCheckModule(
-      "\\func test (A : \\Type) (x : A) (p : x = x) : p = p =>\n" +
-      "  \\case \\elim x, p \\with {\n" +
-      "    | _, _ => {?}\n" +
-      "  }", 2);
+    typeCheckModule("""
+      \\func test (A : \\Type) (x : A) (p : x = x) : p = p =>
+        \\case \\elim x, p \\with {
+          | _, _ => {?}
+        }
+      """, 2);
     assertThatErrorsAre(elimSubstError("p"), goal(2));
   }
 
   @Test
   public void checkElimTypeError3() {
-    typeCheckModule(
-      "\\func test (A : \\Type) (x : A) (p : x = x) : p = p =>\n" +
-      "  \\case \\elim p, \\elim x \\with {\n" +
-      "    | _, _ => {?}\n" +
-      "  }", 1);
+    typeCheckModule("""
+      \\func test (A : \\Type) (x : A) (p : x = x) : p = p =>
+        \\case \\elim p, \\elim x \\with {
+          | _, _ => {?}
+        }
+      """, 1);
     assertThatErrorsAre(elimSubstError("p"));
   }
 
   @Test
   public void elimContextTest() {
-    typeCheckModule(
-      "\\func test (x : Nat) (p : x = x) =>\n" +
-      "  (\\case \\elim x, p : x = x \\with {\n" +
-      "    | _, _ => 0\n" +
-      "  }) Nat.+ (\\case x, p : x = x \\with {\n" +
-      "    | _, _ => 1\n" +
-      "})");
+    typeCheckModule("""
+      \\func test (x : Nat) (p : x = x) =>
+        (\\case \\elim x, p : x = x \\with {
+          | _, _ => 0
+        }) Nat.+ (\\case x, p : x = x \\with {
+          | _, _ => 1
+      })
+      """);
   }
 
   @Test
   public void letElimTest() {
-    typeCheckModule(
-      "\\data Or (A B : \\Type) | inl A | inr B\n" +
-      "\\func test (f : Nat -> Nat) : Or (f 0 = 0) (\\Sigma (n : Nat) (f 0 = suc n)) =>\n" +
-      "  \\let x => f 0\n" +
-      "  \\in \\case \\elim x \\return Or (x = 0) (\\Sigma (n : Nat) (x = suc n)) \\with {\n" +
-      "    | 0 => inl idp\n" +
-      "    | suc n => inr (n, idp)\n" +
-      "  }");
+    typeCheckModule("""
+      \\data Or (A B : \\Type) | inl A | inr B
+      \\func test (f : Nat -> Nat) : Or (f 0 = 0) (\\Sigma (n : Nat) (f 0 = suc n)) =>
+        \\let x => f 0
+        \\in \\case \\elim x \\return Or (x = 0) (\\Sigma (n : Nat) (x = suc n)) \\with {
+          | 0 => inl idp
+          | suc n => inr (n, idp)
+        }
+      """);
   }
 
   @Test
@@ -183,27 +196,30 @@ public void funcLevelTest() {
 
   @Test
   public void propertyLevelTest() {
-    typeCheckModule(
-      "\\truncated \\data Trunc (A : \\Type) : \\Prop | in A\n" +
-      "\\record R | field {A : \\Set} (p : \\Pi (a a' : A) -> a = a') (t : Trunc A) : \\level A p\n" +
-      "\\func test : R \\cowith | field _ t => \\case t \\with { | in a => a }");
+    typeCheckModule("""
+      \\truncated \\data Trunc (A : \\Type) : \\Prop | in A
+      \\record R | field {A : \\Set} (p : \\Pi (a a' : A) -> a = a') (t : Trunc A) : \\level A p
+      \\func test : R \\cowith | field _ t => \\case t \\with { | in a => a }
+      """);
   }
 
   @Test
   public void propertyLevelError() {
-    typeCheckModule(
-      "\\truncated \\data Trunc (A : \\Type) : \\Prop | in A\n" +
-      "\\record R | field {A : \\Set} (p : \\Pi (a a' : A) -> a = a') (t : Trunc A) : A\n" +
-      "\\func test : R \\cowith | field _ t => \\scase t \\with { | in a => a }", 1);
+    typeCheckModule("""
+      \\truncated \\data Trunc (A : \\Type) : \\Prop | in A
+      \\record R | field {A : \\Set} (p : \\Pi (a a' : A) -> a = a') (t : Trunc A) : A
+      \\func test : R \\cowith | field _ t => \\scase t \\with { | in a => a }
+      """, 1);
     assertThatErrorsAre(Matchers.typecheckingError(TruncatedDataError.class));
   }
 
   @Test
   public void propertyExtendsLevelTest() {
-    typeCheckModule(
-      "\\truncated \\data Trunc (A : \\Type) : \\Prop | in A\n" +
-      "\\record R | field {A : \\Set} (p : \\Pi (a a' : A) -> a = a') (t : Trunc A) : \\level A p\n" +
-      "\\record S \\extends R | field _ t => \\case t \\with { | in a => a }");
+    typeCheckModule("""
+      \\truncated \\data Trunc (A : \\Type) : \\Prop | in A
+      \\record R | field {A : \\Set} (p : \\Pi (a a' : A) -> a = a') (t : Trunc A) : \\level A p
+      \\record S \\extends R | field _ t => \\case t \\with { | in a => a }
+      """);
   }
 
   @Test
@@ -215,40 +231,44 @@ public void varSubstTest() {
   public void elimTypeTest() {
     TypedBinding n = new TypedBinding("n", ExpressionFactory.Nat());
     Expression type = FunCallExpression.make(Prelude.PATH_INFIX, LevelPair.SET0, Arrays.asList(ExpressionFactory.Nat(), new ReferenceExpression(n), new SmallIntegerExpression(0)));
-    typeCheckExpr(Arrays.asList(n, new TypedBinding("p", type)),
-      "\\case \\elim n, p \\with {\n" +
-      "  | 0, _ => idp\n" +
-      "  | suc _, p => p\n" +
-      "}", type);
+    typeCheckExpr(Arrays.asList(n, new TypedBinding("p", type)), """
+      \\case \\elim n, p \\with {
+        | 0, _ => idp
+        | suc _, p => p
+      }
+      """, type);
   }
 
   @Test
   public void elimTypeTest2() {
     TypedBinding n = new TypedBinding("n", ExpressionFactory.Nat());
     Expression type = FunCallExpression.make(Prelude.PATH_INFIX, LevelPair.SET0, Arrays.asList(ExpressionFactory.Nat(), new ReferenceExpression(n), new SmallIntegerExpression(0)));
-    typeCheckExpr(Arrays.asList(n, new TypedBinding("p", type)),
-      "\\case \\elim n, p \\return n = 0 \\with {\n" +
-      "  | 0, _ => idp\n" +
-      "  | suc _, p => p\n" +
-      "}", null);
+    typeCheckExpr(Arrays.asList(n, new TypedBinding("p", type)), """
+      \\case \\elim n, p \\return n = 0 \\with {
+        | 0, _ => idp
+        | suc _, p => p
+      }
+      """, null);
   }
 
   @Test
   public void elimArgTypeTest() {
-    typeCheckModule(
-      "\\lemma test (f : Nat -> Nat) (p : f 0 = 0) : f 0 = 0 =>\n" +
-      "  \\case f 0 \\as x, \\elim p : x = 0 \\return x = 0 \\with {\n" +
-      "    | _, p => p\n" +
-      "  }");
+    typeCheckModule("""
+      \\lemma test (f : Nat -> Nat) (p : f 0 = 0) : f 0 = 0 =>
+        \\case f 0 \\as x, p : x = 0 \\return x = 0 \\with {
+          | _, p => p
+        }
+      """);
   }
 
   @Test
   public void argTypeTest() {
-    typeCheckModule(
-      "\\func test (f : Nat -> Nat) (p : f 0 = 0) : Nat =>\n" +
-      "  \\case p : Nat \\with {\n" +
-      "    | p => 0\n" +
-      "  }", 1);
+    typeCheckModule("""
+      \\func test (f : Nat -> Nat) (p : f 0 = 0) : Nat =>
+        \\case p : Nat \\with {
+          | p => 0
+        }
+      """, 1);
     assertThatErrorsAre(typeMismatchError());
   }
 
@@ -260,32 +280,44 @@ public void typeTest() {
 
   @Test
   public void depTest() {
-  typeCheckModule(
-    "\\data D (n : Nat) | con1 | con2\n" +
-    "\\func foo (n : Nat) (d : D n) : n = n\n" +
-    "  | 0, con1 => idp\n" +
-    "  | 0, con2 => idp\n" +
-    "  | suc n, con1 => idp\n" +
-    "  | suc n, con2 => idp\n" +
-    "\\lemma test (g : Nat -> Nat) (f : \\Pi (n : Nat) -> D n) : foo (g 0) (f (g 0)) = idp\n" +
-    "  => \\case g 0 \\as x, f x \\as y \\return foo x y = idp \\with {\n" +
-    "    | 0, con1 => idp\n" +
-    "    | 0, con2 => idp\n" +
-    "    | suc x, con1 => idp\n" +
-    "    | suc x, con2 => idp\n" +
-    "  }");
+  typeCheckModule("""
+    \\data D (n : Nat) | con1 | con2
+    \\func foo (n : Nat) (d : D n) : n = n
+      | 0, con1 => idp
+      | 0, con2 => idp
+      | suc n, con1 => idp
+      | suc n, con2 => idp
+    \\lemma test (g : Nat -> Nat) (f : \\Pi (n : Nat) -> D n) : foo (g 0) (f (g 0)) = idp
+      => \\case g 0 \\as x, f x \\as y \\return foo x y = idp \\with {
+        | 0, con1 => idp
+        | 0, con2 => idp
+        | suc x, con1 => idp
+        | suc x, con2 => idp
+      }
+    """);
   }
 
   // TODO: Fix this
   @Ignore
   @Test
   public void elimDepTest() {
-    typeCheckModule(
-      "\\func f (n : Nat) : Nat\n" +
-      "  | 0 => 0\n" +
-      "  | suc n => n\n" +
-      "\\func test (n : Nat) : Nat => \\case \\elim n, f n \\as x, idp : f n = x \\with {\n" +
-      "  | n, e, p => 0\n" +
-      "}");
+    typeCheckModule("""
+      \\func f (n : Nat) : Nat
+        | 0 => 0
+        | suc n => n
+      \\func test (n : Nat) : Nat => \\case \\elim n, f n \\as x, idp : f n = x \\with {
+        | n, e, p => 0
+      }
+      """);
+  }
+
+  @Test
+  public void elimWithTypeTest() {
+    typeCheckModule("""
+      \\func Type-isSet4 {A : \\hType} {x : A} (p : x = x) : p = idp
+        => \\case x \\as x_, \\elim p : x_ = x \\with {
+          | x, idp => idp
+        }
+      """, 1);
   }
 }