Isomorphisms between the coherent models of the lambda-calculus

It is proved that there exists a formula of first-order logic with only one non-logical symbol, a binary function symbol Ap signifying application, which uniformly defines inclusion in all BF(E)-models Some definability results give an isomorphism between the group of bi-stable Ap -automorphisms of A and the group of permutations of A ; it also implies that each BF(E)-model is determined, up to isomorphism, by the cardinal of its set of atoms.