Say that forall x it is true that f x == g x using simple structural equality on the return values. Should f == g? (Q1)
Seems reasonable, but then you have to prove arbitrary function equality. So you can choose “no” for technical reasons, but shouldn’t (\x -> x + 1) equal (\x -> 1 + x)? (Q2)
It seems like those are equal, but for technical reasons, one would need to argue that these are definitely not equal.
Point is, you can choose “only syntactic equality counts” but I personally don’t think it’s a better design. It can be implemented, but I think (\x -> x + 1) is equal to (\x -> 1 + x) and would not be comfortable saying otherwise.
Anyway, hopefully Q1 and Q2 are helpful to your inquiry into function equality more generally. I know equality is a topic of debate/discussion in dependently typed languages, so I bet there are Coq resources that might give a more complete analysis of different concepts of equality.