This merge requests changes the typing, subtyping, environment splitting and environment copying judgments to be Plain, by wrapping them in a plainly modality. Furthermore, it fixes the proofs the typing rules for copy- and adds some missing rules.
This is based on the copying branch, hence that branch should probably be merged first.