| w16_S t n' ⇒ S (nat_of_w16_aux t n')
].
ndefinition nat_of_w16 : word16 → nat ≝ λn:word16.nat_of_w16_aux n (w16_to_recw16 n).
| w16_S t n' ⇒ S (nat_of_w16_aux t n')
].
ndefinition nat_of_w16 : word16 → nat ≝ λn:word16.nat_of_w16_aux n (w16_to_recw16 n).