How to use 'apply ... with' and 'apply ... in' together?

Question

I know that apply f in H can be used to apply a hypothesis to a function, and I know that apply f with a b c can be used to supply the arguments it cannot infer on its own while applying f directly.

Would it be possible to use the two combined somehow?

Answer 1

I would recommend looking at the reference manual: https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.apply-in.

You can use apply f with ... in h with a binding list

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

but it seems that the version with just terms is reserved to apply. This is a bit heavier but should be able to get the same results.