induction タクティクのページの校正

LeanByExample/Tactic/Induction.lean

@@ -1,14 +1,6 @@
 /- # induction
 
-`induction` は、帰納法のためのタクティクです。
-
-たとえば、Lean では自然数 `Nat` は以下のように定義されています。
-
-* `0` は自然数。
-* `succ : Nat → Nat` という関数がある。つまり `n` が自然数ならば `succ n` も自然数。
-* 上記のルールによって自然数だとわかるものだけが自然数。
-
-このように、「既に `A` だとわかっているものから、`A` を作り出すルール」を定めることで `A` という概念を構成するというやり方を、**帰納的(inductive)** であるといいます。帰納的に定義されたものに対して何か証明しようとしているとき、帰納法を使うことが自然な選択になります。
+`induction` は、帰納法のためのタクティクです。自然数 [`Nat`](#{root}/Type/Nat.md) や連結リスト [`List`](#{root}/Type/List.md) など、帰納的に定義されたものに対して何か証明しようとしているとき、帰納法を使うことが自然な選択になります。
 
 典型的な例は、自然数に対する数学的帰納法です。前提として、ある述語 `P : Nat → Prop` に対して `∀ n, P n` を示そうとしているとします。このとき、以下を示せば十分であるというのが、数学的帰納法の主張です。