Coq：別の仮説を適用する方法

Question

コンテキスト内に2つの仮説があるとします（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. 

は、必要な操作を行う必要があります。