diff --git a/tests/lean/run/def2.lean b/tests/lean/run/def2.lean
new file mode 100644
index 0000000000..088cf178b7
--- /dev/null
+++ b/tests/lean/run/def2.lean
@@ -0,0 +1,21 @@
+new_frontend
+
+inductive Vec.{u} (α : Type u) : Nat → Type u
+| nil  : Vec α 0
+| cons : α → {n : Nat} → Vec α n → Vec α (n+1)
+
+open Vec
+universes u
+
+variables {α : Type u}
+variables (f : α → α → α)
+
+def mapHead1 : {n : Nat} → Vec α n → Vec α n → Vec α n
+| _, nil, nil => nil
+| _, cons a va, cons b bv => cons (f a b) va
+
+theorem ex1 : mapHead1 f nil nil = nil :=
+rfl
+
+theorem ex2 (a b : α) (n : Nat) (va vb : Vec α n) : mapHead1 f (cons a va) (cons b vb) = cons (f a b) va :=
+rfl
diff --git a/tests/lean/run/def3.lean b/tests/lean/run/def3.lean
new file mode 100644
index 0000000000..ac41679e8e
--- /dev/null
+++ b/tests/lean/run/def3.lean
@@ -0,0 +1,10 @@
+new_frontend
+
+abbrev N := Nat
+
+def f : N → Nat
+| 0   => 1
+| n+1 => n
+
+theorem ex1 : f 0 = 1 :=
+rfl