Could some semantic equivalence proofs be simpler?

[jaccokrijnen]

Local transformations such as desugaring and wrap/unwrap cancel could perhaps be a stronger equivalence (instead of step-index LR):

desugar t t' -> t ==>[k] v -> t' ==>[j] v

i.e. they will terminate with the exact (syntactic) same value. The proof structure may be much simpler.