Theorem 1 (Böhm, 1968) Let $Λ$ be the set of closed normal forms, and let $S1$ and $S2$ be arbitrary λ-terms. For any non η-equivalent terms $T1, T2 ∈ Λ$ there exists a λ-term $∆$ such that the application of $∆$ to $T1$ evaluates to $S1$ and the application of $∆$ to $T2$ evaluates to $S2$. source
Is there an algorithm to find λ-term $∆$ for a given $T1, T2$?
A similar question was asked and answered. I read the whole paper referenced in the answer. But there is no mention of the real algorithm and whether the procedure is decidable. It just tells us that it is enough to use 3 types of λ-terms to discriminate $T1, T2$:
The hard part is to choose which λ-terms to use and what is the order.
Yes. Gérard Huet, “An Analysis of Böhm’s Theorem” (1993) explains his implementation in ML, and Ben Lynn has another well-explained implementation in Haskell that you can try out on the web page.