diff --git a/tests/lean/simplifier20.lean b/tests/lean/simplifier20.lean
new file mode 100644
index 000000000..bb9b6584d
--- /dev/null
+++ b/tests/lean/simplifier20.lean
@@ -0,0 +1,31 @@
+/- Basic rewriting with eq and generic congruence, with no conditionals -/
+
+namespace test_congr
+
+constants a b c : nat
+axiom H1 : a = b
+axiom H2 : a = c
+
+attribute H1 [simp]
+attribute H2 [simp]
+
+#simplify eq env 0 a -- c
+
+attribute H1 [simp] [priority 20000]
+
+#simplify eq env 0 a -- b
+
+attribute H2 [simp] [priority 30000]
+
+#simplify eq env 0 a -- c
+
+attribute H1 [simp] [priority 20000]
+
+#simplify eq env 0 a -- c
+
+attribute H2 [simp] [priority 20000]
+attribute H1 [simp] [priority 20001]
+
+#simplify eq env 0 a -- b
+
+end test_congr
diff --git a/tests/lean/simplifier20.lean.expected.out b/tests/lean/simplifier20.lean.expected.out
new file mode 100644
index 000000000..bd0911c16
--- /dev/null
+++ b/tests/lean/simplifier20.lean.expected.out
@@ -0,0 +1,5 @@
+c
+b
+c
+c
+b
diff --git a/tests/lean/simplifier21.lean b/tests/lean/simplifier21.lean
new file mode 100644
index 000000000..866ad4ca6
--- /dev/null
+++ b/tests/lean/simplifier21.lean
@@ -0,0 +1,28 @@
+/- Basic rewriting with eq and generic congruence, with no conditionals -/
+
+namespace test_congr
+
+constants a b c : nat
+axiom H1 : a = b
+axiom H2 : a = c
+
+attribute H1 [simp]
+attribute H2 [simp]
+
+#simplify eq env 0 a -- c
+
+attribute H1 [simp]
+
+#simplify eq env 0 a -- b
+
+attribute H1 [simp] [priority std.priority.default+1]
+attribute H2 [simp]
+
+#simplify eq env 0 a -- b
+
+attribute H2 [simp] [priority std.priority.default+2]
+attribute H1 [simp] [priority std.priority.default+1]
+
+#simplify eq env 0 a -- c
+
+end test_congr
diff --git a/tests/lean/simplifier21.lean.expected.out b/tests/lean/simplifier21.lean.expected.out
new file mode 100644
index 000000000..02c2efff3
--- /dev/null
+++ b/tests/lean/simplifier21.lean.expected.out
@@ -0,0 +1,4 @@
+c
+b
+b
+c