在软件基础书籍（已存档）中specialize，引入了该策略作为简化假设的一种方法。
我不明白，为什么这是证明中的有效步骤。
提供的示例增加了我的困惑：
Theorem specialize_example: forall n,
(forall m, m*n = 0)
-> n = 0.
Proof.
intros n H.
specialize H with (m := 1).
simpl in H.
rewrite add_comm in H.
simpl in H.
apply H. Qed.
当我用 替换假设时(forall m, m*n = 0) -> n = 0.，1*n = 0 -> n = 0.我发现我们现在正在成功证明n=0新假设。
我不明白为什么这被接受作为原始定理的证明forall n, (forall m, m*n = 0) -> n = 0.。我们现在不是在继续证明一个新定理吗forall n, 1*n = 0 -> n = 0.？
新定理的证明如何推广为原定理的有效证明？
文中将该specialize策略描述为“本质上只是和的组合”assertapply。也许使用and而
不是将这个（或使用的另一个示例）的证明脚本重写specialize为另一个证明脚本可能会清除问题。assertapplyspecialize