proposition: Lemma nodes_preserved_var : forall (cfg cfg' : BDDconfig) (node : ad), nodes_preserved cfg cfg' -> is_internal_node cfg node -> var cfg' node = var cfg node.
proof: Proof. unfold nodes_preserved, is_internal_node in |- *. intros. inversion H0. inversion H1. inversion H2. unfold var in |- *. rewrite H3. rewrite (H x x0 x1 node H3). 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