proposition: Lemma bool_fun_zero_one_eq : ~ bool_fun_eq bool_fun_zero bool_fun_one.
proof: Proof. unfold bool_fun_eq, bool_fun_zero, bool_fun_one in |- *. unfold not in |- *. intro H. unfold bool_fun_eval in H. cut (false = true). intro; discriminate. apply H. exact (fun x : BDDvar => true). Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2