0

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
  ============================
   ....

So, basically I instantiate IHl' with l'. Is there any tactic which does this ? Rewriting or even introducing a new specialized hypothesis should do.

Sibi
  • 47,472
  • 16
  • 95
  • 163
  • 2
    This type of question crops up from time to time here. Here is a (possibly incomplete) list of questions in chronological order, which might help you: [1](http://stackoverflow.com/questions/15573794/), [2](http://stackoverflow.com/questions/19053778/), [3](http://stackoverflow.com/questions/20156622/), [4](http://stackoverflow.com/questions/25687981/), [5](http://stackoverflow.com/questions/29316168/), [6](http://stackoverflow.com/questions/35994491/), [7](http://stackoverflow.com/questions/39904991/), [8](http://stackoverflow.com/questions/40448703/). – Anton Trunov Apr 11 '17 at 05:32
  • @AntonTrunov BTW Shouldn't some of these questions be marked as duplicates of other ones? – Zimm i48 Apr 12 '17 at 10:32
  • @Zimmi48 I think you are right. I just wanted to increase the connectivity (it may result in better search results). Feel free to flag the questions as you find appropriate :) – Anton Trunov Apr 12 '17 at 10:36
  • Possible duplicate of [Best way to perform universal instantiation in Coq](http://stackoverflow.com/questions/25687981/best-way-to-perform-universal-instantiation-in-coq) – Zimm i48 Apr 12 '17 at 10:41

1 Answers1

2

Just to leave the shortest answer for future ref: specialize IHl' with l'.

I highly recommend you have a look to @Anton's comment anyway.

Vinz
  • 5,997
  • 1
  • 31
  • 52