Prove semantics_11, after updating the shol semantics

Updates based on a read-through with Scott.
Mainly: we know very specifically what (part of) the type of an abs/rep
constant looks like, so don't need to use INST to magic up a type
substitution but can read the desired arguments directly.