如何将(介绍)假设返回到目标公式？

Question

证明:

Parameter A B : Prop.
Goal A->B.
intro A.

我明白了:

 1 subgoals
A : A
______________________________________(1/1)
B

我如何返回A目标部分？返回:

1 subgoals
______________________________________(1/1)
A -> B

Answer 1

使用revert策略:

revert A.

这恰恰相反intro,参见 参考手册.