proposition: Lemma boundedness_preservation : forall bs bs' : BDDstate, (forall (a l r : ad) (x : BDDvar), MapGet _ bs a = Some (x, (l, r)) -> MapGet _ bs' a = Some (x, (l, r))) -> forall (n : BDDvar) (node : ad), BDDbounded bs node n -> BDDbounded bs' node n.
proof: Proof. intros bs bs' H n node H0. elim H0. intro n0. apply BDDbounded_0. intro n0. apply BDDbounded_1. intros node0 n0 x l r H1 H2 H3 H4 H5 H6 H7. apply BDDbounded_2 with (x := x) (l := l) (r := r). apply H. assumption. assumption. assumption. assumption. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat