我试图证明预定义的加法函数是关联的，但我被困在目标读取的步骤上
plus (S x') (plus y z) = plus (plus (S x') y) z
但我唯一的假设是：
IHx' : forall y z : nat,
plus x' (plus y z) = plus (plus x' y) z
此时应该使用函数加号的定义，例如使用函数来评估目标，如cbn(simpl或lazy也可以(。然后你得到了一个目标，你的归纳假设适用，这样你就可以完成congruence.
顺便说一句，当x = 0时的基本情况可以简单地通过计算来求解，因此reflexivity就足够了。
你已经证明了plus 0 x = x，但你也可以(容易地(证明plus (S x) y = S (plus x y)。如果你这样做，你可以把你的目标改写成S (plus x' (plus y z)) = S (plus (plus x' y) z)，然后你可以用你的归纳假设重写。