diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 59df747054..b097689ea4 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -262,7 +262,10 @@ expr type_checker::infer_proj(expr const & e, bool infer_only) {
     }
     r = whnf(r);
     if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
-    return binding_domain(r);
+    r = binding_domain(r);
+    if (is_prop(type) && !is_prop(r))
+        throw invalid_proj_exception(env(), m_lctx, e);
+    return r;
 }
 
 /** \brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not.
diff --git a/tests/lean/unsound.lean b/tests/lean/unsound.lean
new file mode 100644
index 0000000000..9bc1833063
--- /dev/null
+++ b/tests/lean/unsound.lean
@@ -0,0 +1,3 @@
+def foo (h : ∃ x: Nat, True) := h.1
+theorem contradiction : False :=
+  (by decide : 0 ≠ 1) (show foo ⟨0, trivial⟩ = foo ⟨1, trivial⟩ from rfl)
diff --git a/tests/lean/unsound.lean.expected.out b/tests/lean/unsound.lean.expected.out
new file mode 100644
index 0000000000..5aa44c511b
--- /dev/null
+++ b/tests/lean/unsound.lean.expected.out
@@ -0,0 +1,4 @@
+unsound.lean:1:4-1:7: error: (kernel) invalid projection
+  h.1
+unsound.lean:3:28-3:31: error: unknown identifier 'foo'
+unsound.lean:3:47-3:50: error: unknown identifier 'foo'