Defining propositions recursively

Hello. I am trying to solve exercise from “Software Foundations Volume 1” for 3 days already.
I do not belong to any course or university (learning coq myself, do not have any tutor).

Chapter Logic in Coq.

Exercise: 2 stars, standard (In_map_iff)

I have problems with induction: how can I get rid of l = l’ in induction hypothesis? Please see attached screen.

Thank you.

Have you tried dropping eqn:E from the induction? The eqn:E clause should not be necessary for this proof; by dropping that clause, l should disappear from your context entirely, including from the induction hypothesis, and your proof should become easier.

1 Like

Indeed @Natasha, you could say that 99% of the work involved in induction is selecting the right amount of hypotheses that induction should use [both adding and removing]