Use substitutions rather than open (close c x) e

[aseemr]

The typing rules in Pulse and Reflection were written when we did not have substitutions as first class entities. As a result, rules often say open (close c x) e to mean subst [NT x e] c etc. We should migrate to the latter version; one advantage is that the latter is directly amenable to substitution lemmas.