Added the note about translations and approved as 5 kyu

OK, I'll agree to approve it as 5 kyu on the grounds that it will not be accepting Coq and Lean (and Agda?) translations.

(would need a clear and obvious note in the description. About the "no translations to..." I mean)

I disagree. In Idris it is not very easy. 5 kyu is a good rank for this kata. Even in Software Foundations this is a 5 stars exercise.

This kata should not be translated to Coq and Lean. An Agda translation may be possible but I need to see how much Agda can prove automatically.

This Kata should only be approved at white level (i.e. 7-8 kyu) since it only covers the fundamentals of propositional logic.

Opening this as an Issue to prevent approval, until the average assessed rank drops to 7 kyu or below.

Got it and thanks.

Please add the definition of NN from Preloaded to the description.

But I think it is better to avoid this definition and change the definition of DoubleNegationElim in the description:

DoubleNegationElim = (a : Type) -> Not (Not a) -> a