Lemma: Substitution and canonical forms

If

with disjoint contexts, then

In a context consisting only of runtime names, values of types $\mathsf{Q},\mathsf{Bit},1$, tensor, and function are respectively names, bits, $\ast$, pairs, and abstractions.

Proof. Induct on the typing derivation for substitution. A multiplicative rule places $x$ in one premise. In a conditional, $x$ occurs either in the guard context or in the shared alternative context. In the latter case substitute in both alternatives and reuse the same inserted context $\Delta$ in the additive rule. Canonical forms follow from the value grammar and possible final typing rules.