test: for issue #387

closes #387

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]