proposition: Lemma bool_fun_neq_lemma : forall bf1 bf2 : bool_fun, ~ bool_fun_eq bf1 bf2 -> ~ bool_fun_eq bf2 bf1.
proof: Proof. unfold not in |- *; intros. apply H. apply bool_fun_eq_symm. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2