- cst : ℤ → omega.int.preterm
- var : ℤ → ℕ → omega.int.preterm
- add : omega.int.preterm → omega.int.preterm → omega.int.preterm
exprterm, except that all exprs are now replaced with
de Brujin indices of type
nat. This is akin to generalizing over
the terms represented by the said exprs.
Return a term (which is in canonical form by definition) that is equivalent to the input preterm