diff --git a/tests/lean/simp17.lean b/tests/lean/simp17.lean
new file mode 100644
index 000000000..facb8e33c
--- /dev/null
+++ b/tests/lean/simp17.lean
@@ -0,0 +1,15 @@
+rewrite_set simple
+add_rewrite and_truer and_truel and_falser and_falsel or_falsel Nat::add_zeror : simple
+(*
+  add_congr_theorem("simple", "and_congrr")
+*)
+
+variables a b c : Nat
+
+(*
+local t = parse_lean([[c + 0 ≠ b + 1 ∧ b = 0 ∧ c = 1]])
+local s, pr = simplify(t, "simple")
+print(s)
+print(pr)
+print(get_environment():type_check(pr))
+*)
\ No newline at end of file
diff --git a/tests/lean/simp17.lean.expected.out b/tests/lean/simp17.lean.expected.out
new file mode 100644
index 000000000..13677bbb3
--- /dev/null
+++ b/tests/lean/simp17.lean.expected.out
@@ -0,0 +1,13 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: a
+  Assumed: b
+  Assumed: c
+⊥
+trans (and_congrr
+           (λ C::1 : b = 0 ∧ c = 1,
+              congr (congr2 neq (congr1 0 (congr2 Nat::add (and_elimr C::1))))
+                    (congr1 1 (congr2 Nat::add (and_eliml C::1))))
+           (λ C::1 : ⊥, refl (b = 0 ∧ c = 1)))
+      (and_falser (b = 0 ∧ c = 1))
+(c + 0 ≠ b + 1 ∧ b = 0 ∧ c = 1) = ⊥