I took a stab at it, seems everything is indexed by capabilities which makes sense. There is "Equivalence of ephemeral capabilities" for ephemeral indexing out

I took a stab at it, seems everything is indexed by capabilities which makes sense. There is "Equivalence of ephemeral capabilities" for ephemeral indexing outside of iso and turn. There is "Compatible capabilities with ephemeral modifiers" which shows ephemeral indexing does not matter for compatibility. This is extended to types with "Compatible types" then "define the aliasing operator +, to give us the minimum compatible capability when a new alias to an object has been made" with "Aliasing" presenting the cases. There is "Unaliasing" and that's where I'm checking out. Is there a general theory behind these kind of indexed judgement rules with case splitting?