diff --git a/tests/lean/simp15.lean b/tests/lean/simp15.lean
new file mode 100644
index 000000000..ef70d07e3
--- /dev/null
+++ b/tests/lean/simp15.lean
@@ -0,0 +1,17 @@
+rewrite_set simple
+add_rewrite and_truer and_truel and_falser and_falsel or_falsel : simple
+(*
+  add_congr_theorem("simple", "and_congr")
+  add_congr_theorem("simple", "or_congr")
+*)
+
+variables a b c : Nat
+
+(*
+local opts = options({"simplifier", "contextual"}, false)
+local t = parse_lean([[a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a)]])
+local s, pr = simplify(t, "simple", get_environment(), context(), opts)
+print(s)
+print(pr)
+print(get_environment():type_check(pr))
+*)
\ No newline at end of file
diff --git a/tests/lean/simp15.lean.expected.out b/tests/lean/simp15.lean.expected.out
new file mode 100644
index 000000000..b15fb9d5e
--- /dev/null
+++ b/tests/lean/simp15.lean.expected.out
@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: a
+  Assumed: b
+  Assumed: c
+a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a)
+refl (a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a))
+(a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a)) = (a = 1 ∧ (¬ b = 0 ∨ c ≠ 0 ∨ b + c > a))