diff --git a/tests/lean/simplifier9.lean b/tests/lean/simplifier9.lean
index 431ad89e5..ce3a71cfb 100644
--- a/tests/lean/simplifier9.lean
+++ b/tests/lean/simplifier9.lean
@@ -1,8 +1,8 @@
 -- Rewriting with (tmp)-local hypotheses
 import logic.quantifiers
 
-attribute congr_forall [congr]
 attribute congr_imp [congr]
+attribute congr_forall [congr]
 
 universe l
 constants (T : Type.{l}) (P Q : T → Prop)
@@ -22,7 +22,8 @@ constants (x y : T)
 
 #simplify iff env 0 ∀ (p : Prop) (H : ∀ x, P x ↔ Q x), p ∨ P x
 #simplify iff env 0 (∀ (x : T), P x ↔ Q x) →  P x
-#simplify iff env 0 (∀ (x : T), P x ↔ Q x) →  P x
 #simplify iff env 0 ∀ (x y : T), (∀ (x : T), P x ↔ Q x) →  P x
 
+#simplify iff env 0 ∀ (x z : T), x = z → P x
+#simplify iff env 0 ∀ (x y z : T), x = y → y = z → P x
 #simplify iff env 0 ∀ (x z : T), x = z → (∀ (w : T), P w ↔ Q w) →  P x
diff --git a/tests/lean/simplifier9.lean.expected.out b/tests/lean/simplifier9.lean.expected.out
index 168531564..c896ae03d 100644
--- a/tests/lean/simplifier9.lean.expected.out
+++ b/tests/lean/simplifier9.lean.expected.out
@@ -8,6 +8,7 @@ T → T → x = y → P y
 Prop → (∀ (x : T), P x ↔ Q x) → Prop → Q x
 ∀ (x_1 : Prop), (∀ (x : T), P x ↔ Q x) → x_1 ∨ Q x
 (∀ (x : T), P x ↔ Q x) → Q x
-(∀ (x : T), P x ↔ Q x) → Q x
 ∀ (x : T), T → (∀ (x : T), P x ↔ Q x) → Q x
+∀ (x x_1 : T), x = x_1 → P x_1
+∀ (x x_1 x_2 : T), x = x_1 → x_1 = x_2 → P x_2
 ∀ (x x_1 : T), x = x_1 → (∀ (w : T), P w ↔ Q w) → Q x_1