Exactly. Well, mathematicians do that, they encode everything in the type, which they call the theorem or lemma (while the program itself is the proof). But mat

Exactly. Well, mathematicians do that, they encode everything in the type, which they call the theorem or lemma (while the program itself is the proof). But mathematicians, it seems to me, tend to do a lot of proof copy-pasting, unless they use category theory or something like that.