如何使用“应用.与“和”应用..一起

Question

我知道apply f in H可以用来将假设应用于函数，我知道apply f with a b c可以用来提供它在直接应用f时无法自行推断的参数。

是否有可能以某种方式将两者结合使用？

Answer 1

我建议查看参考手册：https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.apply-in。

可以将apply f with ... in h与绑定列表一起使用

apply f with (x := u) (0 := v) in h

但似乎只有条款的版本保留给apply.这有点重，但应该能够得到相同的结果。