I am an university student working on a thesis about λ-calculus. I'd like to know if there's any article or publication about proof assistant formalizations of the Bohm theorem ("any two normal forms in λ-calculus which are not η-convertible are separable"), or more generally about Bohm trees and related topics, so that I can decide whether working on it or doing something else.
I've searched on different sites and archives (Coq library, Isabelle Archive of Formal Proofs, Mizar webpage, this StackExchange forum, the Coq Zulip chat, and I did some direct research on Google) but didn't find anything. Can you suggest any website or other resource where I might find them? Do you already know about any similar article or work?
Thanks in advance