diff --git a/tests/lean/run/eq22.lean b/tests/lean/run/eq22.lean
new file mode 100644
index 000000000..fae15af6a
--- /dev/null
+++ b/tests/lean/run/eq22.lean
@@ -0,0 +1,9 @@
+import data.list
+open list
+
+definition head {A : Type} : Π (l : list A), l ≠ nil → A,
+head nil h      := absurd rfl h,
+head (a :: l) _ := a
+
+theorem head_cons {A : Type} (a : A) (l : list A) (h : a :: l ≠ nil) : head (a :: l) h = a :=
+rfl