Invert

這裡的重點是，既然 $?0$ 已經套用了 $B$ 與 $x$ ，因此就創立關聯它所創立的 lambda $\lambda 1. \lambda 2. \fbox{?}$ 中的變數到其 contextual variables 的映射（mappings）是

1 \mapsto B \\ 2 \mapsto x

現在右手邊的 term 只需要看自己的每個 rigid form 有沒有被指向，只要這個映射裡面查找到有變數是指向 rigid form 自己，即反過來創立 rigid form 指向新名字的映射。比如說我們右手邊的 term 是一個 rigid form $B$ ，因此得到的反映射是

B \mapsto 1