# Unable to use the induction hypothesis in In_map_iff

Hi!

I’m solving this problem from ‘Logic’ and I don’t know how to proceed further. I am unable to use IHl’. Here is my attempt:

If there is a more efficient way to approach this problem, please let me know. Thanks!

When you have a hypothesis `IHl'` that’s an implication and another hypothesis `HB` that matches the premises of `IHl'`, you can apply `IHl'` to `HB` by `apply IHl' in HB`, or `specialize (IHl' HB)` (which is more robust if `IHl'` has more than one premises).

Note also that by using `exists x` in both branches after `intros [HA|HB]`, you’re basically claiming that `In y (map f (x :: l')) -> f x = y /\ In x (x :: l')`. Can you see how that’s quite different from the original goal?

I could understand the `apply IHl' in HB` part, but could not understand the point you made in the second paragraph. How is it `In y (map f(x :: l'))` and not `In y (map f l')`?

You have the goal

``````In y (map f l) -> exists x, f x = y /\ In x l
``````

The tactic `induction l as [|x l' IHl']` destructs `l` and, in the second subgoal, replaces `l` with `(x :: l')`. To avoid the name collision with `exists x`, that gets renamed to `exists x0`.

``````In y (map f (x :: l')) -> exists x0, f x0 = y /\ In x0 (x :: l')
``````

Then the tactic `intros [HA|HB]` destructs the hypothesis `In y (map f (x :: l'))`, and in both cases you instantiate the existential quantifier with `exists x`. The result of that instantiation is the same as if, from the previous goal, you removed the `exists x0` quantifier and replace other occurrences of `x0` with `x`:

``````In y (map f (x :: l')) -> f x = y /\ In x (x :: l')
``````