fact: Definition high (cfg : BDDconfig) (node : ad) := match MapGet _ (fst cfg) node with | None => N0 | Some (x, (l, r)) => r end.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1