Now LF_Empty is a subtype only of judgment types, not of expression types, preserving adequacy.
In the process of moving subordination enforcement from type checking to axiom insertion.
Rename modus_ponens to compose (it was the wrong name).