Comment by unified101

What do u think lean is? That's like saying a program that works, is inscrutable because it appeals to the oracle of "code test cases" to prove itself correct.

You're either being intentionally obtuse, or unintentionally ignorant.