proposition: Lemma high_bounded : forall (cfg : BDDconfig) (node : ad), BDDconfig_OK cfg -> is_internal_node cfg node -> BDDbounded (fst cfg) (high cfg node) (var cfg node).
proof: Proof. intros cfg node H H0. exact (proj2 (proj2 (internal_node_lemma cfg node H H0))). Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2