diff --git a/tests/lean/simp33.lean b/tests/lean/simp33.lean
new file mode 100644
index 000000000..6baaf595d
--- /dev/null
+++ b/tests/lean/simp33.lean
@@ -0,0 +1,9 @@
+import tactic
+variable f {A : TypeU} : A → A
+axiom Ax1 (a : Bool) : f a = not a
+axiom Ax2 (a : Nat)  : f a = 0
+rewrite_set S
+add_rewrite Ax1 Ax2 : S
+theorem T1 (a : Nat) : f (f a > 0)
+:= by simp S
+print environment 1
diff --git a/tests/lean/simp33.lean.expected.out b/tests/lean/simp33.lean.expected.out
new file mode 100644
index 000000000..548ef0bd1
--- /dev/null
+++ b/tests/lean/simp33.lean.expected.out
@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'tactic'
+  Assumed: f
+  Assumed: Ax1
+  Assumed: Ax2
+  Proved: T1
+theorem T1 (a : ℕ) : f (f a > 0) := eqt_elim (trans (congr2 f (congr1 0 (congr2 Nat::gt (Ax2 a)))) (Ax1 ⊥))