proposition: Lemma config_OK_zero : forall cfg : BDDconfig, BDDconfig_OK cfg -> MapGet _ (fst cfg) BDDzero = None.
proof: Proof. intro cfg. elim cfg. clear cfg. intros bs y. elim y. intros share counter. intros H. elim H. intros H0 H1. elim H0. intros H2 H3. simpl in |- *. exact H2. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat