Lemma 3 ([Thinning by insertion]). Suppose Γ M:A , and suppose that Δ is a valid context containing the declarations of Γ unchanged and in their original order. Then Δ M:A .

Induct on the size of the given derivation. For an axiom, weaken through the declarations of Δ . For a variable or weakening rule, split Δ just after the last declaration of the source context. Transport the rule's premises to the part before that declaration by induction, reapply the rule, and then weaken through the remaining suffix. The necessary sorting judgments for that suffix are supplied by validity of Δ . At a binder, first rename its bound variable fresh for Δ . Its domain sorting is a premise of product formation or a smaller subderivation supplied by Lemma 2 ([Validity and scope]). Induction transports this sorting to Δ , making the extended target context valid. Induction therefore also transports the body or codomain premise to that extension. Reapply the original rule. Application and conversion transport their unchanged-context premises and reapply their rule.