-- A typical example that current method does not handle well. -- The current method generates O(n^2) inverse is obtained. double(n) = add(dup(n)) dup(Z) = Pair(Z,Z) dup(S(n)) = dSuc(dup(n)) dSuc(Pair(m,n)) = Pair(S(m), S(n)) add(Pair(Z,m)) = m add(Pair(S(n),m)) = S(add(Pair(n,m)))