[proofplan] We prove the theorem by induction on the derivation tree of the typing judgment $\Gamma\vdash t:A$ in $\mathcal T$. The construction of $\mathsf{CH}(\mathcal T)$ was chosen so that every propositional typing rule of $\mathcal T$ is read as a proof rule, while non-propositional data are retained as parameters. The only points to check are that assumptions, declared constants, structural rules, substitution, and conversion preserve the represented sequent and the proof certificate. Once these cases are verified, the last rule of the typing derivation translates directly into the last rule of a proof derivation in $\mathsf{CH}(\mathcal T)$. [/proofplan] [step:Translate contexts into hypotheses and parameters] Let $\Gamma$ be a well-formed context of $\mathcal T$. Define $\Gamma_{\operatorname{par}}$ to be the ordered list of declarations $x:B$ in $\Gamma$ for which $B$ is not a proposition in the sense of $\mathcal T$. Define $\Gamma_{\operatorname{hyp}}$ to be the ordered list of declarations $x:B$ in $\Gamma$ for which $\Gamma\vdash B:\operatorname{Prop}$ is derivable. By the definition of $\mathsf{CH}(\mathcal T)$, the sequent $\mathsf{Seq}_{\mathsf{CH}}(\Gamma,A)$ is the judgment of the dependent logic whose parameters are the entries of $\Gamma_{\operatorname{par}}$, whose hypotheses are the entries of $\Gamma_{\operatorname{hyp}}$, and whose conclusion is the proposition $A$. This translation is defined only for well-formed contexts and propositions in context. These are exactly the hypotheses in the theorem: $\Gamma$ is well formed and $\Gamma\vdash A:\operatorname{Prop}$ is derivable. Hence the target sequent $\mathsf{Seq}_{\mathsf{CH}}(\Gamma,A)$ is a well-formed sequent of $\mathsf{CH}(\mathcal T)$. [/step] [step:Induct on the typing derivation] Let $\mathcal D$ be a derivation tree in $\mathcal T$ whose conclusion is the typing judgment $\Gamma\vdash t:A$. Define the induction predicate $P(\mathcal D)$ as follows: if the conclusion of $\mathcal D$ is a typing judgment $\Delta\vdash u:B$ and $\Delta\vdash B:\operatorname{Prop}$ is derivable, then $\mathsf{Seq}_{\mathsf{CH}}(\Delta,B)$ is derivable in $\mathsf{CH}(\mathcal T)$ with $u$ as proof certificate. We prove $P(\mathcal D)$ by induction on the height of $\mathcal D$. The induction hypothesis says that $P(\mathcal D_i)$ holds for every immediate premise derivation $\mathcal D_i$ of the last inference rule of $\mathcal D$. [guided] The theorem is a soundness statement for type checking: a derivation accepted by the type-theoretic rules should become a derivation in the associated logic. The natural measure is therefore the height of the derivation tree. Let $\mathcal D$ denote a derivation tree in $\mathcal T$ with conclusion $\Gamma\vdash t:A$. We define the induction predicate carefully because not every intermediate judgment in a type-theoretic derivation is itself a proposition. The predicate $P(\mathcal D)$ applies when the conclusion of $\mathcal D$ is a typing judgment $\Delta\vdash u:B$ and the type $B$ is known to be a proposition, meaning that $\Delta\vdash B:\operatorname{Prop}$ is derivable in $\mathcal T$. In that case $P(\mathcal D)$ asserts that the represented sequent $\mathsf{Seq}_{\mathsf{CH}}(\Delta,B)$ is derivable in $\mathsf{CH}(\mathcal T)$ and that the certificate attached to that proof is exactly the term $u$. This formulation matches the construction of $\mathsf{CH}(\mathcal T)$. Non-propositional judgments are not discarded; they supply parameters, type formation data, substitution data, or equality data needed by the propositional rules. The induction hypothesis is therefore applied only to propositional typing premises, while the non-propositional premises are carried along as the parameter and well-formedness premises required by the corresponding rule of $\mathsf{CH}(\mathcal T)$. [/guided] [/step] [step:Handle assumptions and declared constants] Suppose first that the last rule of $\mathcal D$ is the variable rule and its conclusion is $\Gamma\vdash x:B$ with $\Gamma\vdash B:\operatorname{Prop}$. Then the declaration $x:B$ occurs in $\Gamma_{\operatorname{hyp}}$, so $\mathsf{CH}(\mathcal T)$ has the hypothesis rule deriving $\mathsf{Seq}_{\mathsf{CH}}(\Gamma,B)$ with certificate $x$. Suppose next that the last rule of $\mathcal D$ introduces a declared constant $c:C$ and that $\Gamma\vdash C:\operatorname{Prop}$ after the parameters in $\Gamma$ are fixed. If $C$ is propositional, then by definition $c:C$ is an axiom of $\mathsf{CH}(\mathcal T)$, and weakening by the parameters and hypotheses in $\Gamma$ gives a derivation of $\mathsf{Seq}_{\mathsf{CH}}(\Gamma,C)$ with certificate $c$. If the declared constant has non-propositional type, it is not itself a proof certificate of a proposition; it is retained as a parameter and can occur only inside the formation of later propositions or proof terms. [/step] [step:Translate each propositional typing rule into the corresponding proof rule] Assume the last rule of $\mathcal D$ is a typing rule $R$ whose conclusion is $\Gamma\vdash t:A$ with $\Gamma\vdash A:\operatorname{Prop}$. Let $\mathcal D_1,\dots,\mathcal D_n$ be the immediate premise derivations of this last rule, where $n$ is the number of premises of $R$. For every premise derivation $\mathcal D_i$ whose conclusion is a propositional typing judgment, the induction hypothesis supplies the corresponding proof derivation in $\mathsf{CH}(\mathcal T)$ with the same certificate as in $\mathcal T$. For every premise of $R$ that is a context-formation, type-formation, equality, or non-propositional typing judgment, the definition of $\mathsf{CH}(\mathcal T)$ reads it as a parameter, formation, or equality premise of the corresponding proof rule. By construction of $\mathsf{CH}(\mathcal T)$, the typing rule $R$ has a corresponding proof rule $R^{\mathsf{CH}}$ with the translated premises and conclusion $\mathsf{Seq}_{\mathsf{CH}}(\Gamma,A)$. Applying $R^{\mathsf{CH}}$ to the translated premise derivations gives a derivation of $\mathsf{Seq}_{\mathsf{CH}}(\Gamma,A)$ with certificate $t$. [guided] This is the main Curry–Howard step. Suppose the last inference in the type-checking derivation is a typing rule $R$ ending in the judgment $\Gamma\vdash t:A$, and suppose $A$ is a proposition in context, so $\Gamma\vdash A:\operatorname{Prop}$ is derivable. The rule $R$ has some finite list of immediate premises; call their derivation trees $\mathcal D_1,\dots,\mathcal D_n$. We separate the premises into two kinds. If a premise is itself a propositional typing judgment, then the induction hypothesis applies to its derivation tree. Thus that premise has already been translated into a proof derivation in $\mathsf{CH}(\mathcal T)$, with the same term as proof certificate. If a premise is not a propositional typing judgment, then it is still part of the formal rule data: it may assert that a context is well formed, that a type is formed, that two expressions are judgmentally equal, or that some non-propositional parameter is available. By the definition of $\mathsf{CH}(\mathcal T)$, these premises are exactly the auxiliary premises allowed in the corresponding dependent proof rule. Now use the defining clause of $\mathsf{CH}(\mathcal T)$: every typing rule of $\mathcal T$ whose conclusion is a proof of a proposition is included as the corresponding proof rule of the logic. Therefore the rule $R$ has a translated rule $R^{\mathsf{CH}}$. Its premises are precisely the translated premises just described, and its conclusion is the sequent represented by $\Gamma\vdash A$. Applying $R^{\mathsf{CH}}$ gives a proof of $\mathsf{Seq}_{\mathsf{CH}}(\Gamma,A)$. The certificate is also preserved. The conclusion of $R$ in $\mathcal T$ has certificate term $t$, and the translated proof rule is defined to carry the same certificate. Thus the resulting proof in $\mathsf{CH}(\mathcal T)$ proves the represented sequent with $t$ as its proof certificate. [/guided] [/step] [step:Check structural rules substitution and conversion] If the last rule of $\mathcal D$ is weakening, exchange, contraction where present, or another structural rule of $\mathcal T$, then the translated rule in $\mathsf{CH}(\mathcal T)$ performs the same operation on hypotheses and parameters. The induction hypothesis gives the translated premise sequent with its certificate, and the corresponding structural rule of $\mathsf{CH}(\mathcal T)$ gives the translated conclusion sequent with the same certificate. If the last rule of $\mathcal D$ is substitution, then the premise derivations provide the proof certificate being substituted and the term or parameter substituted for the variable. The definition of $\mathsf{CH}(\mathcal T)$ includes the corresponding substitution rule, so the translated premise derivations yield the translated substituted sequent with the substituted certificate. If the last rule of $\mathcal D$ is conversion, then there are derivations of $\Gamma\vdash t:B$ and $\Gamma\vdash B\equiv A$, with $\Gamma\vdash A:\operatorname{Prop}$. The induction hypothesis applied to the derivation of $\Gamma\vdash t:B$ gives a proof of $\mathsf{Seq}_{\mathsf{CH}}(\Gamma,B)$ with certificate $t$. Since $\mathsf{CH}(\mathcal T)$ respects judgmental equality by construction, the equality premise $\Gamma\vdash B\equiv A$ converts this proof into a proof of $\mathsf{Seq}_{\mathsf{CH}}(\Gamma,A)$ with the same certificate $t$. [/step] [step:Conclude soundness for the original typing judgment] The preceding cases cover every possible last rule in the derivation tree $\mathcal D$ of $\Gamma\vdash t:A$: assumptions, declared constants, propositional typing rules, structural rules, substitution, and conversion. By induction on the height of $\mathcal D$, the predicate $P(\mathcal D)$ holds for the original derivation. Since the conclusion of $\mathcal D$ is $\Gamma\vdash t:A$ and $\Gamma\vdash A:\operatorname{Prop}$ is one of the hypotheses of the theorem, $\mathsf{Seq}_{\mathsf{CH}}(\Gamma,A)$ is derivable in $\mathsf{CH}(\mathcal T)$ with $t$ as proof certificate. This is exactly the claimed Curry–Howard soundness of type checking for the fixed presentation $\mathcal T$. [/step]