Note: at some point, it might be useful to make `term` and `pred` take a
`kinstr` as argument to have a better scope for typechecking.