Their translation won't type check currently. Need to unfold the inner fixpoints to get nested fixpoints as [I].