diff --git a/tests/list.ref b/tests/list.ref
new file mode 100644
index 0000000000000000000000000000000000000000..ac5cc48d46a5a1538950047afc8d239e7b20583d
--- /dev/null
+++ b/tests/list.ref
@@ -0,0 +1,22 @@
+1 goal
+  
+  ============================
+  None = None
+1 goal
+  
+  ============================
+  Some 10 = Some 10
+1 goal
+  
+  ============================
+  Some 11 = Some 11
+1 goal
+  
+  l : list nat
+  ============================
+  last (11 :: l) = last (11 :: l)
+1 goal
+  
+  l : list nat
+  ============================
+  last (10 :: l) = last (10 :: l)
diff --git a/tests/list.v b/tests/list.v
new file mode 100644
index 0000000000000000000000000000000000000000..dd1d58fbb880ee1d2a14263a896c317001e3df13
--- /dev/null
+++ b/tests/list.v
@@ -0,0 +1,17 @@
+From stdpp Require Import list.
+
+Lemma last_simpl_test_nil : last [] =@{option nat} None.
+Proof. simpl. Show. done. Qed.
+
+Lemma last_simpl_test_singleton : last [10] = Some 10.
+Proof. simpl. Show. done. Qed.
+
+Lemma last_simpl_test_double : last [10; 11] = Some 11.
+Proof. simpl. Show. done. Qed.
+
+Lemma last_simpl_test_cons_cons l : last (10 :: 11 :: l) = last (11 :: l).
+Proof. simpl. Show. done. Qed.
+
+(* The following should not [simpl] and result in a [match]. *)
+Lemma last_simpl_test_cons l : last (10 :: l) = last (10 :: l).
+Proof. simpl. Show. done. Qed.