用更具体的表达重写假设 [英] 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屋！
查看全文
