diff --git a/examples/ex16.lean b/examples/ex16.lean
new file mode 100644
index 000000000..1c52b7717
--- /dev/null
+++ b/examples/ex16.lean
@@ -0,0 +1,17 @@
+Variable f : Pi (A : Type), A -> Bool
+Show fun (A B : Type) (a : _), f B a
+(* The following one should produce an error *)
+(* Show fun (A : Type) (a : _) (B : Type), f B a *)
+
+Variable myeq : Pi (A : Type u), A -> A -> Bool
+Show  myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b)
+Check myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b)
+
+
+Variable R : Type -> Bool
+Variable h : (Pi (A : Type), R A) -> Bool
+Check (fun (H  : Bool)
+           (f1 : Pi (A : Type), R _)
+           (g1 : Pi (A : Type), R A)
+           (G  : Pi (A : Type), myeq _ (f1 _) (g1 A)),
+           h f1)
diff --git a/examples/ex17.lean b/examples/ex17.lean
new file mode 100644
index 000000000..6aef8a164
--- /dev/null
+++ b/examples/ex17.lean
@@ -0,0 +1,10 @@
+Check fun (A : Type) (a : A),
+          let b := a
+          in b
+
+Variable g : Pi A : Type, A -> A
+
+Definition f (A: Type) (a : A) : A :=
+   let b := g A a,
+       c := g A b
+   in c
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 3367d024a..8de5b593d 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -17,3 +17,5 @@ add_test(lean12 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples
 add_test(lean13 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex13.lean")
 add_test(lean14 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex14.lean")
 add_test(lean15 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex15.lean")
+add_test(lean16 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex16.lean")
+add_test(lean17 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex17.lean")