用更具体的表达重写假设 [英] Rewriting hypothesis with a more concrete expression
本文介绍了用更具体的表达重写假设的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
让我们说这是我当前的前提和目标:
Let's say these are my current premises and goals:
IHl' : forall l' : list A, In a l'' \/ In a l' -> In a (l'' ++ l')
l' : list A
============================
....
现在,我希望假设像这样转变:
Now, I want the hypothesis to get transformed like this:
IHl' : In a l'' \/ In a l' -> In a (l'' ++ l')
l' : list A
============================
....
因此,基本上我实例化了 IHl'
和 l'
。请问这有什么战术吗?
So, basically I instantiate IHl'
with l'
. Is there any tactic which does this ? Rewriting or even introducing a new specialized hypothesis should do.
推荐答案
只是为将来的引用留出了最短的答案:用l'专业化IHl'。
Just to leave the shortest answer for future ref: specialize IHl' with l'
.
我强烈建议您还是看看@Anton的评论。
I highly recommend you have a look to @Anton's comment anyway.
这篇关于用更具体的表达重写假设的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
查看全文