- added definition for targets-effects - consistency relation between
  targets and effects. This is just a wrapper on tgtmap`leq-efxmap,
  since we are only interested on relation between tgtmap and efxmap.

- defined clsmap-cxt-effects, which is a wrapper on clsmap-cxt-efxmap.
- name change
- proved reftyping-consistent with help of a few lemmas (for cases of
- lit and read).