我有一个引理告诉加法通勤：
Lemma commute: for all x y, add x y = add y x.
现在我的目标是要证明：
add (add x (S y)) z = add x (S (add y z))
我想用引理重写左侧的内部加法
[add x (S y)至add (S y) x。
但是，命令rewrite commute改写了外部加法：
[add (add x (S y)) z至add z (add x (S y))。
问题：如何使用通勤重写内部子表达式？
您可以使用：来精确确定引理所需的参数。
rewrite commute with (x := x)(y :=(S y)).但更常见的是将其像函数一样使用：
rewrite (commute x (S y)).如果指定的参数之一显而易见，则可以避免在第一种情况下提及它，或者在第二种情况下使用下划线，这将在此处给出：
rewrite commute with (y :=(S y)).和
rewrite (commute _ (S y)).