proposition: Lemma bool_fun_of_BDD_1_semantics_2 : forall (cfg : BDDconfig) (node : ad) (bound1 bound2 : nat), MapGet _ (fst cfg) node = None -> bool_fun_of_BDD_1 cfg node bound1 = bool_fun_of_BDD_1 cfg node bound2.
proof: Proof. intros cfg node bound1 bound2 H. case bound1. simpl in |- *. case bound2. simpl in |- *. reflexivity. simpl in |- *. rewrite H. trivial. simpl in |- *. rewrite H. case bound2. simpl in |- *. rewrite H. trivial. simpl in |- *. rewrite H. trivial. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1