diff --git a/tests/lean/run/387.lean b/tests/lean/run/387.lean
new file mode 100644
index 0000000000..4125badd8c
--- /dev/null
+++ b/tests/lean/run/387.lean
@@ -0,0 +1,16 @@
+--
+
+axiom p {α β} : α → β → Prop
+axiom foo {α β} (a : α) (b : β) : p a b
+
+example : p 0 0 := by simp [foo]
+example (a : Nat) : p a a := by simp [foo a]
+example : p 0 0 := by simp [foo 0]
+example : p 0 0 := by simp [foo 0 0]
+example : p 0 0 := by
+  simp [foo 1] -- will not simplify
+  simp [foo 0]
+example : p 0 0 ∧ p 1 1 := by
+  simp [foo 1]
+  traceState
+  simp [foo 0]