1: \begin{definition}[Necessity Introduction]\label{def_NecIntro}

2: {\em The restriction on $\intro{\necsy}$ depends on programs synthesized 

3: from the proof of the premise $A$ of this rule, unless all formulas in the context 

4: $\Gamma$ are refutation irrelevant or $A$ is refutation irrelevant, see the 

5: paragraph following Theorem \ref{soundness} in Section \ref{sec_LMD} 

6: below.} Thus input proofs are inductively defined 

7: together with their extracted programs (and their corresponding output proofs).

8: \end{definition}

9: