Removed the old name "Prin" for principals.
Now, we refer only to locations, and use "L.t" directly.
This required some non-trivial changes to proofs.

Moreover, I got rid of a bunch of deprecated stuff.
This was just getting in the way.

This was out of sync with the naming decisions elsewhere.