fact: Definition BDDshare_lookup (share : BDDsharing_map) (x : BDDvar) (l r : ad) : option ad := match MapGet _ share l with | None => None | Some m1 => match MapGet _ m1 r with | None => None | Some m2 => match MapGet _ m2 x with | None => None | Some y => Some y end end end.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat