proposition: Lemma bool_fun_of_BDD_ext : forall (cfg : BDDconfig) (node : ad), bool_fun_ext (bool_fun_of_BDD cfg node).
proof: Proof. unfold bool_fun_of_BDD in |- *. intros cfg node. apply bool_fun_of_BDD_1_ext. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2