proposition: Lemma bool_fun_if_lemma_2 : forall (cfg : BDDconfig) (node : ad), BDDconfig_OK cfg -> is_internal_node cfg node -> bool_fun_eq (bool_fun_of_BDD cfg node) (bool_fun_if (var cfg node) (bool_fun_of_BDD cfg (high cfg node)) (bool_fun_of_BDD cfg (low cfg node))).
proof: Proof. intros cfg node H H0. rewrite (proj2 (proj2 (bool_fun_of_BDD_semantics cfg H)) node H0). unfold bool_fun_eq in |- *. unfold bool_fun_eval in |- *. unfold bool_fun_if in |- *. unfold ifb in |- *. 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