negation_fn_applied_twice
andreykl opened this issue · 3 comments
andreykl commented
Small question. In the Basics in More Exercises we have task negation_fn_applied_twice. I'm not sure we have a way to solve it using just rewrite (it looks like task is to solve it by rewrite). I was not able to solve it by using rewrite (replace has helped). I'm not sure if it its just me or the task requires a bit more knowledge.
clayrat commented
Hello, you can solve it with rewrite if at the end you reuse a lemma that has been introduced before.
andreykl commented
could you check irc, pls when you have a minute to discuss this