Lemma: Branch-wise linearity

If $\Gamma ⊢t:A$, every resource in $\Gamma$ has exactly one free occurrence in every occurrence selection. The free runtime names of $t$ are exactly the runtime names in $\Gamma$, and the two alternatives of a conditional have identical free-runtime-name sets.

Proof. Induct on typing. Multiplicative rules partition contexts. Abstraction removes its bound variable from the free context. For a conditional, the guard uses its own context, and either selected alternative uses the shared alternative context once. The same induction proves equality of the alternatives' name sets.