（本文是对 James Wilcox 的 Exercises on Generalizing the Induction Hypothesis 的一点详细解说，也感谢 James Wilcox 在文章中提供的几道颇有练习价值的证明题！）
由于大多数数据类型常见的递归属性，在 Coq 中使用归纳法证明命题是一件颇为常见且基础的操作。
然而，有些具有递归性质的命题并不易于使用归纳法直接进行证明，原因在于，这些命题中的部分变量取了特定的值，而归纳过程中这些变量的值会发生变化，从而导致归纳过程无法继续下去。对此，我们往往需要找到一个更一般性的命题，用归纳法证明这一一般命题，随后使用该一般命题构建对原命题的证明。
下面便是两道实践此类命题证明方法论的绝佳例题。
继续阅读归纳证明方法论——使用归纳法构建一般性结论的证明