proposition: Lemma nodes_preserved_2 : forall (cfg cfg' : BDDconfig) (node : ad), config_node_OK cfg node -> nodes_preserved cfg cfg' -> config_node_OK cfg' node.
proof: Proof. intros cfg cfg' node H H0. elim H; intro. rewrite H1. left; reflexivity. elim H1; intro. rewrite H2; right; left; reflexivity. right; right. unfold in_dom in H2. elim (option_sum _ (MapGet (BDDvar * (ad * ad)) (fst cfg) node)). intro y. elim y. intros x. elim x. intro y0. intro y1. elim y1. intros y2 y3 y4. unfold nodes_preserved in H0. unfold in_dom in |- *. rewrite (H0 y0 y2 y3 node y4). reflexivity. intro y. rewrite y in H2. discriminate. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4