Coq: how to apply one hypothesis to another

Assume I have two hypotheses in the context, `a_b : A -> B` and `a : A`. I should be able to apply `a_b` to `a` to gain a further hypothesis, `b : B`. That is, given the following state: ``` 1 subgoal A : Prop B : Prop C : Prop a_b : A -> B a : A ______________________________________(1/1) C ``` There should be some tactic, `foo (a_b a)`, to transform this into the following state: ``` 1 subgoal A : Prop B : Prop C : Prop a_b : A -> B a : A b : B ______________________________________(1/1) C ``` But I don't know what `foo` is. One thing I can do is this: ``` assert B as b. apply a_b. exact a. ``` but this is rather long-winded, and scales badly if instead of `a_b a` I have some larger expression. Another thing I can do is: ``` specialize (a_b a). ``` but this replaces the `a_b` hypothesis, which I don't want to do.