[ cosmetic ] superscripts, model definition

- Minor modification of the typical model: using nf Booleans rather than
  either ne ones or Agda's Bool (truer to the "nf at the base types"
  approach to model constructions).

- Turning \in and \entails into superscripts in the definitions of wk.