Moving on: Recursive subtyping

I began the recursive subtyping section with a motivation of and definition of constraint entailment, then began a description of the type system involved. Some of the definitions will be repeats of the foundations at the top of the paper - there's some overlap in the selftype section too. We can fix that up as we go, it's easier just to lay out what I want to say as I say it for now.

Felix, let me know if there's more work I need to be doing on selftypes first, but it looked technically complete enough to start work on the next paper.

--Carl