A relational programming language for defining and evaluating relations between terms in the simply-typed lambda calculus. Uses Huet's higher-order unification algorithm for equality relations, and a miniKanren-like interface for constructing relations and querying substitutions/solutions to relations with unification variables.