- added some theorems about same-class (respects-eq, U-inversion).
- changed deep-disjoint-join-preserves-clsmap-cxt-tgtmap to
  join-preserves-clsmap-cxt-tgtmap
- proved subtyping consistent, and "write" clause for reftyping-consistent.
- set+set2tgtmap-preserves-fresh (simple copy-and-paste from
  set+nat2tgtmap-preserves-fresh).
- added restriction in subtype, so that read and write sets are
  required to be leq than the fields set.