 Proof. Induction on derivation length. Suppose \(\vdash\)  \(F\). If \(F\) is a member of \(\mathsf{J}_{0}\), or a member of \(CS\), there is a constant \(e_{n}\) (where \(n\) might be 1) such that \(e_{n} : F\) is in \(CS\), since \(CS\) is axiomatically appropriate. Then \(e_{n} : F\) is derivable. If \(F\) is obtained by Modus Ponens from \(X \rightarrow F\) and \(X\), then, by the Induction Hypothesis, \(\vdash s :( X \rightarrow F)\) and \(\vdash t : X\) for some \(s , t\). Using the Application Axiom, \(\vdash [ s\cdot t ]: F\).