val idterm = oabstr (1,ovar 1);

val idtype1 = (tvar 1) --> (tvar 1);

val idtype2 = ((tvar 1) --> (tvar 1))
                 --> (tvar 1) --> (tvar 1);

val idtype3 = ((tvar 1) --> (tvar 1) --> (tvar 1))
                 --> (tvar 1) --> (tvar 1) --> (tvar 1);

val idtype4 = (((tvar 1) --> (tvar 1))
                              --> (tvar 1) --> (tvar 1))
                 --> ((tvar 1) --> (tvar 1))
                                    --> (tvar 1) --> (tvar 1);

val CNtype = ((tvar 1) --> (tvar 1)) --> ((tvar 1) --> (tvar 1));

val add = (oabstr (1, (oabstr (2, (oabstr (3, (oabstr (4,
              (oappl (oappl (ovar 1, ovar 3),
                             oappl (oappl (ovar 2, ovar 3), ovar 4)))))))))));

val mult = (oabstr (1, (oabstr (2, (oabstr (3,
               (oappl (ovar 1, oappl (ovar 2,ovar 3)))))))));

val exp = (oabstr (1, (oabstr (2, (oappl (ovar 1, ovar 2))))));

val zero = (oabstr (1, (oabstr (2, (ovar 2)))));

val one = (oabstr (1, (oabstr (2, (oappl ((ovar 1), (ovar 2)))))));

val twice = (oabstr (1, (oappl (oappl (add, (ovar 1)),(ovar 1)))));

val two = (oappl (oappl (add,one),one));

val twoo = (oappl (twice, one));

val three = (oappl (oappl (add,one),two));

val four = (oappl (oappl (mult,two),two));

val eight = (oappl (oappl (exp,three),two));

val nine = (oappl (oappl (exp,two),three));

val alot = (oappl (oappl (exp,three),eight));