Lemma 31 ([Reduction transport]). A one-step full beta reduction of a typed expression transports its tree to a tree of the reduct at the same expected type. For every environment, good Val and Read evaluations remain good and their …

Construct the transported tree independently of its environment. At contextual steps transport the changed child. A change in a product domain context-converts its open codomain tree. A change in a lambda annotation also transports the supporting product typing by subject reduction and context-converts the open body. A change in an application argument changes its core result type to a convertible one; subject reduction retains the root expectation. Induct on the reduction position, simultaneously for Val and Read. At evaluated children use the induction hypothesis. At binders apply it under every typed raw extension required by goodness; structural invariance handles the context-converted unchanged children. Actual types, gates, and argument keys are unchanged. At a skipped variable-headed spine, a reduction can only be inside its arguments; the head and skipped condition persist. Ignored children need no semantic property, only the transported typing. For a remaining Read with active base projection, apply the Val statement already proved at the same root. A Read outside actual profile S remains default. At a root contraction (λx:D.P)N⟶P[N/x] , generation and product compatibility align the lambda annotation and body type with the application's stored product. Retarget the argument to the annotation type, substitute its tree in the body, and retarget the result to the old expectation. Consider a good active Val. The application cannot have been skipped, since its syntactic head is a lambda. Let K,L be the actual function and result layers, respectively. They are active. By Lemma 26 ([Signs and dependencies]), the actual domain layer I is active whenever it belongs to H . The argument is good if I is active. Evaluation uses the valid normal key (Nξ)^# and, when required, the payload Val (N) . The lambda equation gives its body value with this key, including at an exit where the lambda supplied the correct tag. The raw image Nξ is convertible to its normal form. Structural invariance therefore identifies this body value with the one at the raw image, with the same payload. Lambda goodness supplies body goodness for both typed extensions. Lemma 30 ([Substitution of a good value]) now identifies that value with the beta contractum and proves its goodness. No strong normalization of Nξ was used. For a Read with actual profile in S , a skipped clause at the root is impossible because the head is a lambda. Its goodness therefore provides the active all-shape base projection, and the preceding Val argument applies. This proves the root case and the lemma.