proposition: Lemma bool_fun_neq_one_zero : forall cfg : BDDconfig, BDDconfig_OK cfg -> ~ bool_fun_eq (bool_fun_of_BDD cfg BDDone) (bool_fun_of_BDD cfg BDDzero).
proof: Proof. intros cfg H. unfold bool_fun_eq, bool_fun_zero, bool_fun_one in |- *. unfold bool_fun_eval in |- *. rewrite (proj1 (bool_fun_of_BDD_semantics cfg H)). rewrite (proj1 (proj2 (bool_fun_of_BDD_semantics cfg H))). unfold not in |- *; intros. absurd (false = true). unfold not in |- *; discriminate. unfold bool_fun_zero, bool_fun_one in H0. rewrite (H0 (fun x : BDDvar => true)). reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2