proposition: Lemma nodes_preserved_internal : forall (cfg cfg' : BDDconfig) (node : ad), BDDconfig_OK cfg -> BDDconfig_OK cfg' -> config_node_OK cfg node -> is_internal_node cfg' node -> is_internal_node cfg node.
proof: Proof. intros cfg cfg' node H H0 H1 H2. inversion H2. inversion H3. inversion H4. elim H1. intro H6. rewrite H6 in H5. rewrite (config_OK_zero cfg' H0) in H5. discriminate. intro H6. elim H6; intro. rewrite H7 in H5. rewrite (config_OK_one cfg' H0) in H5. discriminate. apply in_dom_is_internal. 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