diff --git a/tests/lean/exists6.lean b/tests/lean/exists6.lean
new file mode 100644
index 000000000..35fe6579a
--- /dev/null
+++ b/tests/lean/exists6.lean
@@ -0,0 +1,7 @@
+Variable P : Int -> Int -> Int -> Bool
+Axiom Ax1 : exists x y z, P x y z
+Axiom Ax2 : forall x y z, not (P x y z)
+Theorem T : false :=
+    ExistsElim Ax1 (fun a H1, ExistsElim H1 (fun b H2, ExistsElim H2 (fun (c : Int) (H3 : P a b c),
+         let notH3 : not (P a b c) :=  ForallElim (ForallElim (ForallElim Ax2 a) b) c
+         in Absurd H3 notH3)))
diff --git a/tests/lean/exists6.lean.expected.out b/tests/lean/exists6.lean.expected.out
new file mode 100644
index 000000000..6055c3fff
--- /dev/null
+++ b/tests/lean/exists6.lean.expected.out
@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: P
+  Assumed: Ax1
+  Assumed: Ax2
+  Proved: T