diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 12d739ae..cbc2dcde 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -16,7 +16,7 @@
 - [cases: 論理和∨を使う](./cases.md)
 - [choose: 選択関数を得る](./choose.md)
 - [constructor: 論理積∧を示す](./constructor.md)
-- [contradiction: 矛盾](./contradiction.md)
+- [contradiction: 爆発律](./contradiction.md)
 - [conv: 変換モードに入る](./conv.md)
 - [convert: 惜しい補題を使う](./convert.md)
 - [done: 証明終了を宣言](./done.md)
diff --git a/src/contradiction.md b/src/contradiction.md
index 4f8bcd18..22342c6c 100644
--- a/src/contradiction.md
+++ b/src/contradiction.md
@@ -1,6 +1,6 @@
 # contradiction
 
-`contradiction` は，矛盾によりゴールを閉じるタクティクです．矛盾から任意の命題を証明することができます．
+矛盾からはどんな命題でも証明することができます．これを爆発律(principle of explosion)と呼びますが，`contradiction` は，この爆発律を使ってゴールを閉じるタクティクです．
 
 ローカルコンテキストに `P` と `¬ P` が同時にあるなど，矛盾した状況にあるときにゴールを閉じます．