Lemma: Consumption

Under Definition def:names, destructive readout of both names in $B=NA$ has the interface

No legal continuation uses the consumed $N$- or $A$-name as a quantum input.

Proof. The first Enter instruction removes its measured name. The second removes the other measured name. The resulting quantum context contains only the previously retained spectator names. Induction over any subsequent instruction sequence shows that unitary operations preserve this context, classical operations introduce no quantum names, and allocations introduce only globally fresh names. Neither consumed name can reappear.