proposition: Lemma bool_fun_eq_neg : forall bf1 bf2 : bool_fun, bool_fun_eq (bool_fun_neg bf1) (bool_fun_neg bf2) -> bool_fun_eq bf1 bf2.
proof: Proof. unfold bool_fun_eq, bool_fun_neg in |- *. unfold bool_fun_eval in |- *. intros bf1 bf2 H vb. cut (negb (bf1 vb) = negb (bf2 vb)). unfold negb in |- *. elim (bf1 vb). elim (bf2 vb). intro H0. reflexivity. intro H0. rewrite H0. reflexivity. elim (bf2 vb). intro H0. rewrite H0. reflexivity. intro H0. reflexivity. apply H. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1