proposition: Lemma bool_fun_of_BDDzero : forall cfg : BDDconfig, BDDconfig_OK cfg -> bool_fun_eq (bool_fun_of_BDD cfg BDDzero) bool_fun_zero.
proof: Proof. intros cfg H. unfold bool_fun_eq in |- *. unfold bool_fun_eval in |- *. intro vb. rewrite (proj1 (bool_fun_of_BDD_semantics cfg H)). reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2