diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index e0dcee71ed..850a760114 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1739,6 +1739,9 @@ def reduceBool (b : Bool) : Bool := b
   We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection). -/
 def reduceNat (n : Nat) : Nat := n
 
+def ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b := h
+def ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b := h
+
 end Lean
 
 /- Classical reasoning support -/
diff --git a/tests/lean/run/reduce1.lean b/tests/lean/run/reduce1.lean
index 06040b608f..1d99a1ede7 100644
--- a/tests/lean/run/reduce1.lean
+++ b/tests/lean/run/reduce1.lean
@@ -15,3 +15,9 @@ def v2 : Bool := 10000000000000000 < 200000000000000000000
 
 theorem tst2 : Lean.reduceBool v2 = true :=
 rfl
+
+theorem tst3 : v1 = 3628800 :=
+Lean.ofReduceNat v1 3628800 rfl
+
+theorem tst4 : v2 = true :=
+Lean.ofReduceBool v2 true rfl