Theorem: Strong normalization and step bound

Every reduction sequence from a well-typed configuration $[\psi ,t]$ has length at most $m(t)$.

Proof. Every root transition decreases $m$ by at least one. Beta reduction and tuple elimination use Lemma lem:measure; conditional selection uses the maximum. Other transitions remove one counted operation. Along an evaluation-context hole the measure is additive, since the hole is never inside a body or unselected alternative. The same decrease therefore holds contextually.