fact: Definition BDDor_memo_lookup (memo : BDDor_memo) (node1 node2 : ad) := match MapGet _ memo node1 with | None => None | Some m1 => match MapGet _ m1 node2 with | None => None | Some node => Some node end end.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2