diff --git a/Examples/Solution/HeytingAndBooleanAlgebra.lean b/Examples/Solution/HeytingAndBooleanAlgebra.lean
index 631b1516..b412a5a7 100644
--- a/Examples/Solution/HeytingAndBooleanAlgebra.lean
+++ b/Examples/Solution/HeytingAndBooleanAlgebra.lean
@@ -261,14 +261,9 @@ abbrev Three := Fin 3
 
 /- ### 問2.1 半順序集合であること -/
 
--- この二つの定理は使用して良い
-theorem min_def (a b : Nat) : min a b = if a ≤ b then a else b := by aesop
-theorem max_def (a b : Nat) : max a b = if a ≤ b then b else a := by aesop
-
 -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
 -- いくつルールを追加しても構いません。
 --##--
-local add_aesop_rules norm [simp [min_def, max_def]]
 local add_aesop_rules safe [cases Fin]
 local add_aesop_rules norm [simp Fin.le_def]
 local add_aesop_rules safe [tactic (by omega)]
diff --git a/Exercise/HeytingAndBooleanAlgebra.lean b/Exercise/HeytingAndBooleanAlgebra.lean
index 3876dd07..cf13ca2e 100644
--- a/Exercise/HeytingAndBooleanAlgebra.lean
+++ b/Exercise/HeytingAndBooleanAlgebra.lean
@@ -258,10 +258,6 @@ abbrev Three := Fin 3
 
 /- ### 問2.1 半順序集合であること -/
 
--- この二つの定理は使用して良い
-theorem min_def (a b : Nat) : min a b = if a ≤ b then a else b := by aesop
-theorem max_def (a b : Nat) : max a b = if a ≤ b then b else a := by aesop
-
 -- ここに `local add_aesop_rules` コマンドを追加して証明が通るようにしてください。
 -- いくつルールを追加しても構いません。