See weak product.

Check that $\text{fst}(\text{pair}\ M\ N) \sim M$ and $\text{snd}(\text{pair}\ M\ N) \sim N$

Any element can play the role of a weak terminal: $\lambda x. i$ for all $i \in \Lambda / _\sim$

Let $\cdot$ be given by application, if $M \in \Lambda$ induces an operation in $[L \bowtie L, L]$ representing some $f : L \times L \to L$ then $\lambda xy. M(\text{pair}\ x\ y)$ induces the corresponding operation in $L, L \Rightarrow L$; conversely, if $N$ induces an operation in $[L, L \Rightarrow L]$, then $\lambda z. N (\text{fst}\ z) (\text{snd}\ z)$ induces the corresponding one in $[L \bowtie L, L]$.

There is a submodel $\Lambda^0/_\sim$ for closed terms.

Use $\beta$-equivalence then we denote $\Lambda / _{=_\beta}$.