Böhm separation theorem
= Böhm separation theorem
{c}
Two distinct closed <lambda terms> in normal form for both <beta reduction> and <eta conversion> admit a separating context that maps them respectively to the two <Church Booleans>. Finite <Böhm trees> and the <Böhm-out lemma> isolate their first genuine head disagreement. The qualification about <eta conversion> matters: distinct beta-normal forms that are eta-equivalent cannot be separated this way.