`32`
     : Z
[f:(nat->Z)]`(f O)+0`
     : (nat->Z)->Z