Editing Böhm's theorem (section)

== The theorem ==

Let {{$|\Lambda_N}} be the set of all β-normal λ-terms.

Given a λ-term {{$|M}}, we denote by {{$|\overline{M} }} a ''closure'' of {{$|M}}, ''i.e.'' {{$|\overline{M} {{=}} \lambda x_1\dots\lambda x_n.M}} where {{$|x_1,\dots,x_n}} is an enumeration of the free variables of {{$|M}}.

{{Theorem box
|type=theorem
|id=Böhm
|title={{cite|Bohm1968|Böhm 1968}}
|content=Let {{$|M,N \in \Lambda_N}} be β-normal λ-terms. Then either {{$|M{{=}}_\eta N}}, or there are λ-terms {{$|P_1,\dots,P_n}} such that {{$$|
\overline{M}P_1\dots P_n \rightarrow_\beta^* \mathsf{true} 
\quad \text{and} \quad 
\overline{N}P_1\dots P_n \rightarrow_\beta^* \mathsf{false}.}}
}}

Usually one takes {{$|\mathsf{true} {{=}} \lambda x.\lambda y.x}} and {{$|\mathsf{false} {{=}} \lambda x.\lambda y.y}}, but they can be replaced with any other λ-terms {{$|Q_M }} and {{$|Q_N }}: {{$$|
\overline{M}P_1\dots P_nQ_MQ_N \rightarrow_\beta^* Q_M 
\quad \text{and} \quad 
\overline{N}P_1\dots P_nQ_MQ_N \rightarrow_\beta^* Q_N.}}

A proof sketch is given by {{Cite|GuePipDez2009|Guerrini ''et al.'' (2009)}}. The full proof is presented in {{Cite|Barendregt|Barendregt (1984, ch.&nbsp;10)}}. Its constructive fashion is taken seriously by {{Cite|Huet1993|Huet (1993)}}, who presents a CaML code proving the theorem. A simpler proof can be found in {{Cite|Joly2000|Joly (2000, ch.&nbsp;10)}}.
{{Theorem box|type=corollary|id=semantic-corollary|content=If a model equates βη-distinct normal λ-terms, then it equates all λ-terms.}}