proposition: Lemma BDDvar_le_z : forall x : BDDvar, BDDvar_le N0 x = true.
proof: Proof. intro x. unfold BDDvar_le in |- *. unfold Nleb in |- *. simpl in |- *. reflexivity. 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