proposition: Lemma bool_fun_and_is_neg_or_neg_neg : forall bf1 bf2 : bool_fun, bool_fun_eq (bool_fun_and bf1 bf2) (bool_fun_neg (bool_fun_or (bool_fun_neg bf1) (bool_fun_neg bf2))).
proof: Proof. intros. unfold bool_fun_eq, bool_fun_neg, bool_fun_or, bool_fun_and in |- *. unfold bool_fun_eval in |- *. intro. elim (bf1 vb). elim (bf2 vb). reflexivity. reflexivity. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2 bdd6 bdd7 BDDdummy_lemma_2 BDDdummy_lemma_3 BDDdummy_lemma_4 bdd8 bdd9