fact: Definition BDDconfig_OK (cfg : BDDconfig) := match cfg return Prop with | (bs, (share, counter)) => BDDstate_OK bs /\ BDDsharing_OK bs share /\ (forall a : ad, Nleb counter a = true -> MapGet _ bs a = None) /\ Nleb (ad_S (ad_S N0)) counter = true end.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat