The hash function should be invariant under alpha-renaming. Using de Bruijn notation seems to be possible, but it requires alpha-converting the whole tree when a binding is created, and has the unhappy consequence that a substructure of an abt is not a well-formed abs (since the de Bruijn indices are broken). So, is there a good (neat, elegant and/or efficient) way to construct such a function? By the way, is there any study on this matter? Any help is appreciated!