Assume I have two hypotheses in the context, a_b : A -> B
and a : A
. I should be able to apply a_b
to a
to gain a further hypothesis, b : B
.
That is, given the following state:
1 subgoal
A : Prop
B : Prop
C : Prop
a_b : A -> B
a : A
______________________________________(1/1)
C
There should be some tactic, foo (a_b a)
, to transform this into the following state:
1 subgoal
A : Prop
B : Prop
C : Prop
a_b : A -> B
a : A
b : B
______________________________________(1/1)
C
But I don't know what foo
is.
One thing I can do is this:
assert B as b.
apply a_b.
exact a.
but this is rather long-winded, and scales badly if instead of a_b a
I have some larger expression.
Another thing I can do is:
specialize (a_b a).
but this replaces the a_b
hypothesis, which I don't want to do.
pose proof (a_b a) as B.
should do what you want.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With