more permissive type inference for HO term;
helper functions in Lex_ho, to parse decls, terms, etc.