Suponha que eu tenha duas hipóteses no contexto,a_b : A -> B ea : A. Eu deveria ser capaz de aplicara_b paraa para ganhar uma outra hipótese,b : B.

Isto é, dado o seguinte estado:

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

Deve haver alguma tática,foo (a_b a), para transformar isso no seguinte estado:

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

Mas eu não sei o quefoo é.

Uma coisa que posso fazer é isto:

 assert B as b.
 apply a_b.
 exact a.

mas isso é bastante longo, e escala muito se em vez dea_b a Eu tenho uma expressão maior.

Outra coisa que posso fazer é:

specialize (a_b a).

mas issosubstitui aa_b hipótese, que eu não quero fazer.