measure f :: Int -> Int

one :: {v:Int| f v == v}
one = 1