如何一起使用“apply ... with”和“apply ... in”？

Question

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

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

Answer 1

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

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

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

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