English: huggermugger. It's so confusing (hugger + mugger = clandestine work) that you cannot just pass by it without rising an eyebrow.

Polish: dykteryjka (short, funny story) and imponderabilia (things which are incalculable, but affect other things, like luck, state of mind, or similar).

What's your process of learning Coq? I have to confess that 'proof automation' is one of those shortcomings I never overcame. Even going through your well-documented code took me a shameful amount of time, and that's after you've done all the heavy lifting.

Agreed on Idris, but, per your recommendation back from IRC dwelling days, I found Type-Driven Development with Idris by E. Brady as much more accessible. In this case, it means "I went farther into it than into any Coq tutorial". :P

Tip for future QM problems: write n subscripts in phi and normalization factor. It's sometimes easy to lose the explicit relationship, and it's one of those omissions that can waste a lot of your time when it's least convenient.

Thanks, I'll give it a look sometime. Not much of a fan of 'prequels', but this looks both interesting and promising.

Also, sorry for using an alt.