-- 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)))
