proposition: Lemma BDDalloc_allocates : forall (cfg : BDDconfig) (l r : ad) (x : BDDvar), MapGet _ (fst (fst (BDDalloc cfg x l r))) (snd (BDDalloc cfg x l r)) = Some (x, (l, r)).
proof: Proof. intro cfg. elim cfg. clear cfg. intros bs y0. elim y0. clear y0. intros share counter l r x. simpl in |- *. rewrite (MapPut_semantics (BDDvar * (ad * ad)) bs counter (x, (l, r)) counter) . cut (N.eqb counter counter = true). intro H. rewrite H. trivial. apply Neqb_correct. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat