This is the notion of extensional equality. You are correct that this is effectively impossible to implement in a programming language. On the other hand, it is possible to implement intensional equality, which is what I am interested in. (Note: functions do not need to be pure to be compared for intensional equality)