fact: Definition augment (vb : var_binding) (x : BDDvar) (b : bool) (y : BDDvar) := if BDDvar_eq x y then b else vb y.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2