diff --git a/tests/playground/som.lean b/tests/playground/som.lean
index 36798302c3..88d5f2c975 100644
--- a/tests/playground/som.lean
+++ b/tests/playground/som.lean
@@ -216,3 +216,8 @@ theorem Expr.toPoly_denote (ctx : Context α) (e : Expr) : e.toPoly.denote ctx =
   | add a b => simp! [Poly.add_denote, *]
   | mul a b => simp! [Poly.mul_denote, *]
   | sub a b => simp! [Poly.add_denote, *, sub_def, Poly.neg_denote, mul_one, mul_comm]
+
+theorem Expr.eq_of_toPoly_eq (ctx : Context α) (a b : Expr) (h : a.toPoly == b.toPoly) : a.denote ctx = b.denote ctx := by
+  have h := congrArg (Poly.denote ctx) (eq_of_beq h)
+  simp [toPoly_denote] at h
+  assumption