相关疑难解决方法(0)

假设我在上下文中有两个假设,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. …