proposition: Lemma initBDDstate_OK : BDDstate_OK initBDDstate.
proof: Proof. unfold BDDstate_OK, initBDDstate in |- *. split. simpl in |- *. trivial. split. simpl in |- *. trivial. intros a H. compute in H. discriminate H. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat