**new feature**: simple types for terms. Enough infrastructure has been added for
parsing TFF0 to be (at least theoretically) possible. Also, curryfied terms are well typed