On the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms for the canonical notion of $\delta$-reduction

In this paper we consider a substitution and inheritance property, which is the necessary and sufficient condition for the uniqueness of $\beta\delta$-normal form of typed $\lambda$-terms, for canonical notion of $\delta$-reduction. Typed $\lambda$-terms use variables of any order and constants of order $\leq1$, where the constants of order $1$ are strongly computable, monotonic functions with indeterminate values of arguments. The canonical notion of $\delta$-reduction is the notion of $\delta$-reduction that is used in the implementation of functional programming languages.