fact: Definition BDDordered (bs : BDDstate) (node : ad) := match MapGet _ bs node with | None => True | Some (n, _) => BDDbounded bs node (ad_S n) end.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat