我々の TDPE: 例
= reify(?f. ?n. f @? (n +? (1 +? 2)))= ?x. reify((?f. ?n. f @? (n +? (1 +? 2))) @ x)= ?x. reify(?n. x @? (n +? (1 +? 2)))= ?x. ?y. reify((?n. x @? (n +? (1 +? 2))) @ y)= ?x. ?y. reify(x @? (y +? (1 +? 2)))= ?x. ?y. reify(x @? (y +? 3))= ?x. ?y. reify(x @? (y + 3))