diff --git a/tests/lua/ind6.lua b/tests/lua/ind6.lua
new file mode 100644
index 000000000..ba84b5bab
--- /dev/null
+++ b/tests/lua/ind6.lua
@@ -0,0 +1,18 @@
+
+local env = environment()
+local u   = param_univ("u")
+local Set = Const("Set", {u})
+local A   = Local("A", mk_sort(u))
+
+env = add_inductive(env,
+                     "Set", {u}, 0, mk_sort(u+1),
+                     "sup", Pi(A, mk_arrow(mk_arrow(A, Set), Set)))
+
+local env = environment()
+local u   = param_univ("u")
+local Set = Const("Set", {u})
+local A   = Local("A", mk_sort(u))
+
+env = add_inductive(env,
+                    "Set", {u}, 1, Pi(A, mk_sort(u+1)),
+                    "sup", Pi(A, mk_arrow(mk_arrow(A, Set(A)), Set(A))))