Finish up Subtyping

We need to make sure that we have all the subtyping rules.

All rules that have been added to the paper, but are not yet formalised are unticked here:

• Dual left/right
• Dual unfoldings of send/receive: dual <!> A. S <: <?> A. dual S, <!> A. dual S <: dual <?> A. S etc.
• Dual unfoldings of select/branch
• Unfoldings of append
• Append associativity rules
• Append identity rules
• Swap rule for select/recv
• Swap rule for send/branch
• Swap rule for select/branch
• Forall elimination: ∀X.A <: A[K/X] (Needs update to ∀ with value restriction)
• Exist elimination: A[K/X] <: ∃X.A
• Update Send rule with quantifiers
• Update Recv rule with quantifiers
• Send rule for quantifier instantiation: chan !{X, X}A.S <: chan !{X}A[K/X].S[K/X]
• Recv rule for quantifier instantiation: chan ?{X}A[K/X].S[K/X] <: chan ?{X, X}A.S