let inv_d0 = function
  TTNZ (n) -> n |
  _ -> failwith ("inv_d0 : requires a non-zero even natural number as its argument")