Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax