proposition: Lemma bool_fun_neg_semantics : forall (bf : bool_fun) (vb : var_binding), (bool_fun_eval bf vb = true -> bool_fun_eval (bool_fun_neg bf) vb = false) /\ (bool_fun_eval bf vb = false -> bool_fun_eval (bool_fun_neg bf) vb = true).
proof: Proof. intros bf vb. unfold bool_fun_eval in |- *. unfold bool_fun_neg in |- *. unfold negb in |- *. elim (bf vb). auto. auto. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1