Refinement types often use SMT solvers to automate program verification.
However, since SMT solvers are first-order, verification of properties
that requires higher-order reasoning is not possible.
Proof by Logical Evaluation (PLE) is an algorithm that
provides a layer between refinement types and SMT solvers that
permits symbolic evaluation of functions, but it lacks support for
higher-order reasoning.
We introduce PLEX, an extension to PLE, that supports $\eta$-expansions,
$\beta$-reductions, and dependent
pattern matching. We prove that PLEX is sound and
terminating, describe its implementation in Liquid Haskell, and evaluate
it on examples that make essential use of
higher-order data, and as such they cannot be handled by PLE. The new
PLEX algorithm bridges the gap between higher-order languages and first-order
SMT solvers via refinement types.