proposition: Lemma nodes_preserved_var_1 : forall (cfg cfg' : BDDconfig) (node : ad), BDDconfig_OK cfg -> BDDconfig_OK cfg' -> nodes_preserved cfg cfg' -> config_node_OK cfg node -> var cfg' node = var cfg node.
proof: Proof. intros. unfold var in |- *. elim H2; intro. rewrite H3. rewrite (config_OK_zero cfg H). rewrite (config_OK_zero cfg' H0). reflexivity. elim H3; intro. rewrite H4. rewrite (config_OK_one cfg H). rewrite (config_OK_one cfg' H0). reflexivity. cut (is_internal_node cfg node). intro. inversion H5. inversion H6. inversion H7. rewrite H8. unfold nodes_preserved in H1. rewrite (H1 x x0 x1 node H8). reflexivity. 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