译文为: ``` - [unfold]:用目标中的右式替换定义的常量 - [unfold... in H]:用前提中的右式替换定义的常量 ``` 原文为: ``` - unfold: replace a defined constant by its right-hand side in the goal - unfold... in H: ... or a hypothesis ``` 这里的in the goal应当修饰a defined constant,我认为改成 ``` - [unfold]:用常量的右式替换目标中定义的常量 - [unfold... in H]:用常量的右式替换前提中定义的常量 ``` 更合适一些。请指正。