fact: Definition BDDshare_put (share : BDDsharing_map) (x : BDDvar) (l r counter : ad) : BDDsharing_map := let m1 := match MapGet _ share l with | Some y => y | None => newMap (Map ad) end in let m2 := match MapGet _ m1 r with | Some y => y | None => newMap ad end in let m2' := MapPut _ m2 x counter in let m1' := MapPut _ m1 r m2' in MapPut _ share l m1'.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat