proposition: Lemma initBDDconfig_OK : BDDconfig_OK initBDDconfig.
proof: Proof. unfold BDDconfig_OK, initBDDconfig in |- *. split. exact initBDDstate_OK. split. exact initBDDsharing_map_OK. split. intros a H. simpl in |- *. trivial. trivial. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat