Angenommen, ich habe zwei Hypothesen im Zusammenhang,a_b : A -> B unda : A. Ich sollte mich bewerben könnena_b zua eine weitere Hypothese zu gewinnen,b : B.

Das heißt, vorausgesetzt, der folgende Zustand:

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

Es sollte eine Taktik geben,foo (a_b a), um dies in den folgenden Zustand umzuwandeln:

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

Aber ich weiß nicht wasfoo ist.

Eines kann ich tun:

 assert B as b.
 apply a_b.
 exact a.

aber das ist ziemlich langatmig und skaliert schlecht, wenn nichta_b a Ich habe einen größeren Ausdruck.

Eine andere Sache, die ich tun kann, ist:

specialize (a_b a).

aber diesesersetzt dasa_b Hypothese, die ich nicht machen will.