Quint conversion of applied polymorphic operators is typed too narrowly

[shonfeder]

I have been inferring the types of an applied quint operator from the type map recording the types of its arguments and the type of the application. This breaks the coherence checking of the typed builder, since we are ignoring operator polymorphism. We need to instead use the quint lookup table (exposed in informalsystems/quint#852) to type the applied operator with their most generally inferred types at the time of declaration.