CODEWITHSUNDEEP
coq
Sibi
Sibi

Reputation: 48654

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

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

Upvotes: 0

Views: 142

Answers (1)

Vinz
Vinz

Reputation: 6047

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.

Upvotes: 2

Related Questions