diff --git a/tests/lean/run/eq6.lean b/tests/lean/run/eq6.lean
new file mode 100644
index 000000000..1a8784f4d
--- /dev/null
+++ b/tests/lean/run/eq6.lean
@@ -0,0 +1,15 @@
+import data.list
+open list
+
+definition append {A : Type} : list A → list A → list A,
+append nil      l := l,
+append (h :: t) l := h :: (append t l)
+
+theorem append_nil {A : Type} (l : list A) : append nil l = l :=
+rfl
+
+theorem append_cons {A : Type} (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) :=
+rfl
+
+example : append (1 :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) :=
+rfl