-As a consequence of Abella's successful handling of binding, and of the syntactic nature of \bohm's theorem, Abella may be particularly well-suited to host its formalization. But this is not completely straightforward: let's see one example. One $\nabla$ quantifier handles one binder at the object level, but $\lambda$-terms in strong normal form in \fire{} have the form $\lambda x_1\ldots x_n.\,i$ ($i$ is an inert), where the normal form begins with $n$ $\lambda$-abstractions. In order to handle iterated binders, it would seem natural for $\nabla$ to quantify over ``vectors'' of variables, but this is not possible at the moment. In the light of this and other technical complications, the formalization of \bohm's theorem won't be trivial, and will hopefully shed some light on possible drawbacks/improvements in Abella's logic; this is also the reason why the hosting research group is interested in this project.\r
+As a consequence of Abella's successful handling of binding, and of the syntactic nature of \bohm's theorem, Abella may be particularly well-suited to host its formalization. But this is not completely straightforward: let's see one possible obstacle. One $\nabla$ quantifier handles one binder at the object level, but $\lambda$-terms in strong normal form in \fire{} have the form $\lambda x_1\ldots x_n.\,x_j\,f_1\ldots f_m$ ($f$'s are fireballs), where the normal form begins with $n$ $\lambda$-abstractions. In order to handle iterated binders, it would seem natural for $\nabla$ to quantify over ``vectors'' of variables, but this is not possible at the moment. In the light of this and other technical complications, the formalization of \bohm's theorem won't be trivial, and will hopefully shed some light on possible drawbacks/improvements in Abella's logic; this is also the reason why the hosting research group at LIX, Paris is interested in this project.\r