问题描述
我喜欢在目标是暗示（例如 A -> B）的情况下使用 move=> 库中的 ssreflect 策略，使前提成为假设，并使结论成为新的目标。但是，我并不总是想使用 ssreflect。
是否有另一种 Coq 策略可以在不使用 ssreflect 的情况下做同样的事情？
解决方法
您始终可以使用 intros：intros pat 大致相当于 move=> pat。不幸的是，Coq 和 ssreflect 对介绍模式使用不同的语法，因此两者不可互换。
请注意，现在 ssreflect 是 Coq 发行版的一部分，因此您只需执行 From Coq Require Import ssreflect. 即可使用策略语言，而无需安装单独的库。