GetElem のページに、証明付きアクセスも紹介する

Fixes #866

Examples/TypeClass/GetElem.lean

@@ -43,12 +43,13 @@ instance : GetElem (MyList α) Nat α (fun as i => i < as.length) where
 /- ## インデックスアクセスの種類
 コレクション `as` に対して、`i` 番目の要素を取得すると書きましたが、**i 番目の要素があるとは限らない**という問題があります。これに対処するには様々な方法がありえますが、中でも以下のものは専用の構文が用意されています。
 
-* `as[i]`: インデックス `i` が範囲内であることの証明を要求する。ローカルコンテキスト内に `i` が範囲内であることの証明があれば動作する。
+* `as[i]`: インデックス `i` が範囲内であることの証明を自動で構成する。`i` が変数になっていて具体的に計算できないときでも、ローカルコンテキスト内に `i` が範囲内であることの証明があれば動作する。
 * `as[i]?`: 返り値を `Option` に包む。範囲外の場合は `none` を返す
-* `xs[i]!`: `i` が範囲外だった時には panic する。
+* `xs[i]!`: `i` が範囲外だった時には `panic` する。
+* `xs[i]'h`: `i` が範囲内であることの証明 `h` を渡す。
 -/
 
--- 具体的な数値を渡せば、それが範囲内であることを計算してくれる
+-- 具体的な数値を渡せば、それが範囲内であることを自動的に証明してくれる
 #guard [1, 2, 3][2] = 3
 
 #eval show IO Unit from do
@@ -67,3 +68,6 @@ instance : GetElem (MyList α) Nat α (fun as i => i < as.length) where
 
 -- 範囲外なら panic することにして強引に値を取り出す
 #guard Three[2]! = 3
+
+-- インデックスが範囲内であることの証明を明示的に渡す
+#guard Three[2]'(by decide) = 3