proposition: Lemma nodes_preserved_3 : forall (cfg cfg' : BDDconfig) (node : ad), BDDconfig_OK cfg -> BDDconfig_OK cfg' -> nodes_preserved cfg cfg' -> config_node_OK cfg node -> bool_fun_eq (bool_fun_of_BDD cfg' node) (bool_fun_of_BDD cfg node).
proof: Proof. intros cfg cfg' node H H0 H1 H2. apply bool_fun_preservation. assumption. assumption. unfold nodes_preserved in H1. intros x l r a H3. apply H1. assumption. assumption. 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