Require Import Algebra Reflect.

Declare ML Module "btauto_plugin".