proposition: Lemma bool_fun_neg_one : bool_fun_neg bool_fun_one = bool_fun_zero.
proof: Proof. unfold bool_fun_neg, bool_fun_zero, bool_fun_one in |- *. simpl in |- *. trivial. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1