fact: Definition bool_fun_eq (bf1 bf2 : bool_fun) := forall vb : var_binding, bool_fun_eval bf1 vb = bool_fun_eval bf2 vb.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1