Coq 8.15 should be enabled.

Pretty frustrating that you basically have to to know that a certain function exists in order to do this...

For ease of working in an IDE, the entirety of the preloaded section should be in a single codeblock at the end of the description or as a comment in the solution setup.

The link to the paper in the description is broken. Here's a working one:

https://mbodin.github.io/esplorado/itp13.pdf

Fun Kata :)

Freaking prelude! There should be a second solution for this!

Tedious (at least for me), but definitely not 1kyu

I completely agree, this seems significantly easier than some of the other 4-kyu ranked puzzles out there. 6-kyu would seem more adequate.

Do you still get the error? I tried to run it and it worked

Approved :)