proposition: Lemma bool_fun_independent_one : forall (cfg : BDDconfig) (x : BDDvar), BDDconfig_OK cfg -> bool_fun_independent (bool_fun_of_BDD cfg BDDone) x.
proof: Proof. intro cfg. elim cfg; clear cfg; intros bs y. elim y; clear y; intros share counter. intros x H. rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics (bs, (share, counter)) H))) . unfold bool_fun_independent in |- *. intro vb. unfold bool_fun_eval, bool_fun_one in |- *. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2