A work-in-progress proof of the pacman-completeness of Idris. Requires: [email protected]:steshaw/idris-sdl2.git