fact: Definition BDDcompare (x y : BDDvar) := match x, y with | N0, N0 => Datatypes.Eq | N0, Npos _ => Datatypes.Lt | Npos _, N0 => Datatypes.Gt | Npos p1, Npos p2 => Pcompare p1 p2 Datatypes.Eq end.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)