Böhm separation theorem

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.