Lemma 34 ([Labelled metatheory and reduction lifting]). The labelled typing rules have context validity, correctness of types, weakening, typed substitution by terms of the declared modes, context conversion, generation, and subject …

Substitution preserves modes by induction on syntax. A data expression has no free proof variable, so substitution for a proof variable cannot introduce proof syntax into a data expression. Substitution for a data variable uses a data term. At binders, choose fresh names in the same mode class. Context validity follows by rule induction, retaining the sort typing of each declaration from its introduction premise. The proofs of weakening and typed substitution are inductions on typing derivations. Each binder retains its label, and each substituted term has the mode required by that binder or declaration. Context conversion follows by the identity substitution, typing the changed variable at its old type by conversion. Generation follows by removing final conversions and weakenings. None of these arguments compares distinct possible sort assignments. Correctness of types is another rule induction: an expected type is a literal sort or is itself sorted. At application, the function's product type is sorted by induction; generation on that product and typed substitution sort the application's result type. This remains true through conversion and weakening. For confluence, use parallel reduction with homomorphic clauses at every constructor, including annotation children, and a contracting clause only when the application and lambda labels match. Parallel substitution is proved by syntax induction. Every parallel reduct of a term parallel-reduces to its complete development: contract the matching redexes already present in the original term and develop all children. At an unmatched lambda--application pair only the homomorphic clause applies. This proves the triangle property, hence confluence. The reflexive transitive closures of parallel and ordinary reduction agree, since parallel contractions can be performed from the children upwards. Reduction never changes a product's outer constructor or labels. Common reducts therefore give labelled product compatibility, and a product cannot be convertible to a sort. Subject reduction now follows by induction on a typing derivation. At a root beta step, generation and product compatibility identify the lambda's annotation with the application's domain up to conversion. Convert the argument to the annotation type, substitute in the body, and convert the result to the original expected type. A reduction of an application argument changes its substituted result type by conversion. A reduction of a product domain is handled by context conversion in the codomain premise. For a lambda annotation step, reduce the corresponding domain in its supporting product judgment, context-convert its body premise, re-form the lambda, and convert back to the original sorted product type. The other positions, including positions inside annotations, follow by induction. These constructions keep every label. Erasure of typing follows directly by induction on the labelled derivation. It remains to check that an erased redex can be contracted with the labels present. Every syntactic subterm of a typable term has a typing in the appropriate binder context; for an annotation this follows from context validity. Consider the subterm at the erased redex. Its shape is (λ^ i,j x:D.P) @^ i',j Q. The result modes already force the displayed common j . Lambda generation gives a product type with labels (i,j) ; application generation gives a convertible product type with labels (i',j) . Product compatibility forces i=i' . Thus this is a matching labelled redex. Contract it at the same position. Capture-free substitution commutes with erasure, so its erasure is N ; subject reduction gives the asserted judgment and substitution preserves its mode. This applies to any position, including one in a lambda or product annotation. Induction on a finite erased reduction proves the remaining assertions.