Proving Cantor's Theorem in Clojure Using LaTTe

This was my very first experiment with LaTTe (https://github.com/latte-central/LaTTe) and with proof assistants in general. You can remix the short article in nextjournal (using the invite code curryon2018) to start playing around with LaTTe proofs.

This is also a nice explanation of the lambda calculus involved https://latte-central.github.io/LaTTe/102_Lambda_the_ultimat..., still I couldn't find exactly how LaTTe relates to the (I assume) more popular Coq, except both being based on the calculus of constructions. Anyone with some insights?