假设我们有A B C : Prop
给定具有H : A -> B -> C和单个目标A -> B -> C的上下文，
为什么apply H可以完成证明，解决当前和唯一的目标？
我认为apply策略为所应用术语的每个论点生成一个新的目标，如果其结论与当前目标匹配（或一致）。
如果你的目标只是C，你所描述的会发生什么：要从H: A -> B -> C证明C，你必须为A和B提供证人。然而，无论P是什么形状，你目前的情况只是证明P知道P的一个例子。因此，通过apply和H，你提供了足够的信息来实现目标。