diff --git a/examples/ex9.lean b/examples/ex9.lean
new file mode 100644
index 000000000..c335b8f2e
--- /dev/null
+++ b/examples/ex9.lean
@@ -0,0 +1,5 @@
+Variable f : Type -> Bool
+Variable g : Type -> Type -> Bool
+Show forall (a b : Type), exists (c : Type), (g a b) = (f c)
+Check forall (a b : Type), exists (c : Type), (g a b) = (f c)
+Eval forall (a b : Type), exists (c : Type), (g a b) = (f c)