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