Hybrid - a definitional two-level approach to reasoning with higher-order abstract syntax