[Sniffnoy]

I don't know what I might refer you to. Beta reduction requires recognizing subtrees of the form (#T S) (where T and S are any subtrees), eta reduction just requires recognizing subtrees of the form #(T 1) (where T is any subtree).

No idea about animation. It's really not something I'd thought about, I have to say...

[Sniffnoy]

Oops -- I forgot about the non-freeness requirement. So not just any subtree. That makes it trickier. But still not hard, I think.