+ .
+ (* now use:
+ pp FORMULA to print a formula, unreduced
+ pn FORMULA to print the normal form of a formula (when possible)
+ pi FORMULA to print the integer which FORMULA is a Church numeral for (when possible)
+ .
+ alpha_eq FORM1 FORM2 are FORM1 and FORM2 syntactically equivalent (up to alpha-conversion)?
+ this does not do reductions on the formulae
+ *)
+ .
+ pi << $add$ $one$ $two$ >>;;