SMT encoding implicitly curries the type-binder prefix of a function type, to handle the common case of ML types; one more goal in sf-poly goes through