Type [x:nat]<nat> Cases x  of ((S x) as b) => (S b x) end.