(************************************************************************** * Proving functional programs through a deep embedding * * Package of all deep embedding modules * ***************************************************************************) Set Implicit Arguments. Require Export DeepSyntax DeepPrinter DeepSemantics DeepReasoning DeepTactics DeepBuiltin.