diff --git a/tests/lean/run/e18.lean b/tests/lean/run/e18.lean
new file mode 100644
index 000000000..400bc1362
--- /dev/null
+++ b/tests/lean/run/e18.lean
@@ -0,0 +1,23 @@
+inductive nat : Type :=
+| zero : nat
+| succ : nat → nat
+
+inductive list (A : Type) : Type :=
+| nil {} : list A
+| cons   : A → list A → list A
+
+inductive int : Type :=
+| of_nat : nat → int
+| neg : nat → int
+
+coercion of_nat
+
+variables n m : nat
+variables i j : int
+variable l : list nat
+
+check cons i (cons i nil)
+check cons n (cons n nil)
+check cons i (cons n nil)
+check cons n (cons i nil)
+check cons n (cons i (cons m (cons j nil)))
\ No newline at end of file
diff --git a/tests/lua/level3.lua b/tests/lua/level3.lua
new file mode 100644
index 000000000..6f8325196
--- /dev/null
+++ b/tests/lua/level3.lua
@@ -0,0 +1,17 @@
+local g   = mk_global_univ("g")
+local g1  = mk_level_succ(g)
+local g2  = mk_level_succ(g1)
+local g3  = mk_level_succ(g2)
+local g1b = mk_level_succ(mk_global_univ("g"))
+assert(mk_level_max(g, g1) == g1)
+assert(mk_level_max(g2, g1) == g2)
+assert(mk_level_max(g3, g2) == g3)
+assert(mk_level_max(g2, g3) == g3)
+assert(mk_level_max(g1b, g2) == g2)
+assert(mk_level_max(g1b, g) == g1b)
+assert(mk_level_max(g, g1b) == g1b)
+assert(not (mk_level_max(mk_global_univ("g2"), g1b) == g1b))
+
+assert(mk_level_imax(g2, g3) == g3)
+assert(not (mk_level_imax(g3, g) == g3))
+assert(mk_level_imax(g3, g1) == g3)