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.