proposition: Lemma BDDsharing_lookup_semantics : forall (bs : BDDstate) (share : BDDsharing_map) (n l r : ad) (x : BDDvar), BDDsharing_OK bs share -> (BDDshare_lookup share x l r = Some n <-> MapGet _ bs n = Some (x, (l, r))).
proof: Proof. auto. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat