Supongamos que tengo dos hipótesis en el contexto,a_b : A -> B ya : A. Debería poder aplicara_b aa para ganar una hipótesis más,b : B.

Es decir, dado el siguiente estado:

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

Debe haber alguna táctica,foo (a_b a), para transformar esto en el siguiente estado:

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

Pero no se quefoo es.

Una cosa que puedo hacer es esto:

 assert B as b.
 apply a_b.
 exact a.

pero esto es bastante largo, y se escala mal si en lugar dea_b a Tengo una expresión más grande.

Otra cosa que puedo hacer es:

specialize (a_b a).

pero estoreemplaza laa_b Hipótesis, que no quiero hacer.