Załóżmy, że mam dwie hipotezy w kontekście,a_b : A -> B ia : A. Powinienem móc złożyć wnioseka_b doa zdobyć kolejną hipotezę,b : B.

To znaczy, biorąc pod uwagę następujący stan:

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

Powinna istnieć jakaś taktyka,foo (a_b a), aby przekształcić to w następujący stan:

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

Ale nie wiem cofoo jest.

Jedno, co mogę zrobić, to:

 assert B as b.
 apply a_b.
 exact a.

ale to jest dość długie i źle skaluje się, jeśli zamiasta_b a Mam większe wyrażenie.

Inną rzeczą, którą mogę zrobić, jest:

specialize (a_b a).

ale tozastępuje a_b hipoteza, której nie chcę robić.