Is there a pair of different lambda terms in the normal form that behave identically when applied to any input? Let f and g be lambda terms in the normal form, such that f is intensionally different from g - that is, their string representation using bruijn indexes isn't the same. Is there any choice of f and g such that, for any x that is also a lambda term, f x == g x?
The result you are looking for is Böhm's theorem. The equivalence described by "behaves the same way on all inputs" is the same as the equivalence given by normal forms, but only if you treat eta-equivalent normal forms (λx.Ix and I) as equivalent. You could disallow the former as a normal forms (eta-short) and then you'd have the syntactic condition you want by Böhm's theorem, if I'm not mistaken.