diff --git a/tests/lean/974.lean b/tests/lean/974.lean
index 45a00cd0b0..195fb2bf85 100644
--- a/tests/lean/974.lean
+++ b/tests/lean/974.lean
@@ -13,3 +13,8 @@ attribute [simp] Formula.count_quantifiers
 #check @Formula.count_quantifiers._eq_1
 #check @Formula.count_quantifiers._eq_2
 #check @Formula.count_quantifiers._eq_3
+
+@[simp] def Formula.count_quantifiers2 : Formula n → Nat
+| imp f₁ f₂ => f₁.count_quantifiers2 + f₂.count_quantifiers2
+| all f     => f.count_quantifiers2 + 1
+| _         => 0