Dearest friends,
please give me a hint. see attached file, my question in green
I am absolutely sure that I solved this task finally (second book),
https://softwarefoundations.cis.upenn.edu/current/plf-current/Equiv.html
Exercise: 4 stars, advanced, optional (optimize_0plus)
My understanding is that a fix expression must be applied to a term that begins with a constructor before it can be reduced, which the abstract term c does not. If you try induction c, you should be able to simplify the expression with simpl and such.
In general fix is not quite like fun because it is specifically part of the elimination rules of inductively defined datatypes, and the reduction rule is not beta reduction but “iota” reduction. You can find some references here and here.
Now I understand. Thank you.
