PROGRAM=PROOF
https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf
#Agda
#Curry-Howard同型対応