induction ... generalizing 構文とその制約を紹介する

[Seasawher]

induction で指定した仮定の中に登場する変数は generalize できないという制約がある。理由も含めてわかりやすく説明したい。