proposition: Lemma internal_node_not_constant : forall (cfg : BDDconfig) (node : ad), BDDconfig_OK cfg -> is_internal_node cfg node -> ~ bool_fun_eq (bool_fun_of_BDD cfg node) bool_fun_zero /\ ~ bool_fun_eq (bool_fun_of_BDD cfg node) bool_fun_one.
proof: Proof. intros cfg node H H0. apply internal_node_not_constant_1 with (n := nat_of_N (var cfg node)). assumption. assumption. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2