main(x) = fst(x)

fst(Pair(x,y)) = x

idNat(S(x)) = S(s) where s = idNat(x)
idNat(Z)    = Z

