[maxbendick]

I'm happy to see people learning the Curry–Howard isomorphism the fun way.