Lambda Prolog isn't a "pure" HOL. It's a very restricted form of HOL using Higher-Order Hereditary Herrop formulas, granting us pretty solid generalized mechanisms of implication and universal quantification, which itself more or less means we get contextual reasoning and scoping rules baked into the grammar for free.

Implementing other programming languages and proving theorems are the low-hanging fruits since you get variable binding without name management, but I genuinely think it has profound implications for expert systems since it essentially removes a massive amount of complexity from contextual reasoning. Being able to account for patient history when providing a diagnosis, for example.