Had a meeting with william, talked about refinements and stuff. I started babbling about the "substitution-form" of LF that I've been playing with because I thought it would be a nicer way of handling Σ-types, but after thinking about it a little more it seems unlikely to make the notational headache go away entirely...