Coq：如何將一個假設應用於另一個假設

Question

假設我在上下文中有兩個假設a_b : A -> B和a : A。我應該可以將a_b應用於a以獲得進一步的假設，b : B。

也就是說，給出以下狀態：

1 subgoal 
A : Prop 
B : Prop 
C : Prop 
a_b : A -> B 
a : A 
______________________________________(1/1) 
C 

應該有一些戰術，foo (a_b a)，以將其轉化成以下狀態：

1 subgoal 
A : Prop 
B : Prop 
C : Prop 
a_b : A -> B 
a : A 
b : B 
______________________________________(1/1) 
C 

但我不知道是什麼foo是。

有一件事我可以做的是這樣的：

assert B as b. 
apply a_b. 
exact a. 

但這是比較囉嗦和體重秤如果不好，而不是a_b a我有一些較大的表達。

我可以做的另一件事是：

specialize (a_b a). 

但這取代的a_b假設，這是我不想做的事。

Answer 1

pose proof (a_b a) as B. 

應該做你想做的。