1: \begin{definition}[Theorem]

2: %%%%%  Let $\aenv=\aenv(\prog)$ be the set of axioms for some program \prog.

3: %%%%%  Then

4: %%%%%  $\typ\defeq\tbind{x_1}{\typ_1} \rightarrow \dots \rightarrow \tbind{x_n}{\typ_n} \rightarrow \ttreft{v}{\btyp}{\refa}$

5: %%%%%  is a theorem if

6: %%%%%  $\freevars{\refa} \subseteq \{x_1, \dots, x_n\} \cup \domain{\aenv}$,

7: %%%%%  and for simplicity $\freevars{\typ_i} = \emptyset$.

8: %%%%%

9: %%%%%  Moreover, every expression $e'$ such that  \hastype{\aenv}{e'}{\typ}

10: %%%%%  provides a proof of the theorem $\typ$ with respect to the definitions in \prog.

11: %%%%%  \end{definition}

12: