diff --git a/tests/lean/sig5.lean b/tests/lean/sig5.lean
new file mode 100644
index 000000000..f05b7cbd7
--- /dev/null
+++ b/tests/lean/sig5.lean
@@ -0,0 +1,9 @@
+variable vec : Nat → Type
+definition vec_with_len := sig len, vec len
+variable n : Nat
+variable v : vec n
+check tuple n, v
+check (have vec_with_len : tuple n, v)
+check (let v2 : vec_with_len := tuple n, v
+       in v2)
+check (tuple vec_with_len : n, v)
diff --git a/tests/lean/sig5.lean.expected.out b/tests/lean/sig5.lean.expected.out
new file mode 100644
index 000000000..9193e5ce6
--- /dev/null
+++ b/tests/lean/sig5.lean.expected.out
@@ -0,0 +1,10 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: vec
+  Defined: vec_with_len
+  Assumed: n
+  Assumed: v
+tuple n, v : ℕ ⨯ vec n
+let have_expr : vec_with_len := tuple (sig x : ℕ, vec x) : n, v in have_expr : vec_with_len
+let v2 : vec_with_len := tuple (sig x : ℕ, vec x) : n, v in v2 : vec_with_len
+tuple vec_with_len : n, v : sig len : ℕ, vec len