diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index 19953fb4f..9187f2788 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -290,3 +290,9 @@ namespace nat
 
   lemma sub_lt_succ (a b : ℕ) : a - b < succ a := lt_succ_of_le (sub_le a b)
 end nat
+
+namespace nat_esimp
+  open nat
+  attribute add mul sub [unfold 2]
+  attribute of_num [unfold 1]
+end nat_esimp
diff --git a/hott/init/num.hlean b/hott/init/num.hlean
index 5e67d8aa7..a38e9dd93 100644
--- a/hott/init/num.hlean
+++ b/hott/init/num.hlean
@@ -130,4 +130,4 @@ namespace nat
   num.rec zero
     (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
 end nat
-attribute nat.of_num [reducible] [constructor] -- of_num is also reducible if namespace "nat" is not opened
+attribute nat.of_num [reducible] -- of_num is also reducible if namespace "nat" is not opened
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 6033c5fff..18e4f1dbc 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -247,3 +247,9 @@ namespace nat
   theorem sub_lt_succ_iff_true [simp] (a b : ℕ) : a - b < succ a ↔ true :=
   iff_true_intro !sub_lt_succ
 end nat
+
+namespace nat_esimp
+  open nat
+  attribute add mul sub [unfold 2]
+  attribute of_num [unfold 1]
+end nat_esimp
diff --git a/library/init/num.lean b/library/init/num.lean
index ca83897be..2884e7da2 100644
--- a/library/init/num.lean
+++ b/library/init/num.lean
@@ -127,4 +127,4 @@ namespace nat
   num.rec zero
     (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
 end nat
-attribute nat.of_num [reducible] [constructor] -- of_num is also reducible if namespace "nat" is not opened
+attribute nat.of_num [reducible] -- of_num is also reducible if namespace "nat" is not opened
diff --git a/tests/lean/693.lean b/tests/lean/693.lean
index ef3008ecb..34f9c9064 100644
--- a/tests/lean/693.lean
+++ b/tests/lean/693.lean
@@ -1,4 +1,4 @@
-open nat
+open nat nat_esimp
 
 definition foo [unfold 1 3] (a : nat) (b : nat) (c :nat) : nat :=
 (a + c) * b
diff --git a/tests/lean/693.lean.expected.out b/tests/lean/693.lean.expected.out
index 1e7240e2f..b14394183 100644
--- a/tests/lean/693.lean.expected.out
+++ b/tests/lean/693.lean.expected.out
@@ -1,7 +1,7 @@
 693.lean:10:2: proof state
 c : ℕ,
 h : c = 1
-⊢ (1 + 0) * c = (1 + 0) * 1
+⊢ 1 * c = 1
 693.lean:18:2: proof state
 b c : ℕ,
 h : c = 1
@@ -13,4 +13,4 @@ h : c = 1
 693.lean:34:2: proof state
 b c : ℕ,
 h : c = 1
-⊢ (1 + 1) * c = foo c 1 1
+⊢ 2 * c = foo c 1 1