proposition: Lemma nat_sum : forall n : nat, {m : nat | n = S m} + {n = 0}.
proof: Proof. intro n. elim n. right. reflexivity. intros n0 H. left. split with n0. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4