proposition: Lemma BDDvar_max_x_x : forall x : BDDvar, BDDvar_max x x = x.
proof: Proof. unfold BDDvar_max in |- *. unfold BDDvar_le in |- *. intro x. rewrite (Nleb_refl x). 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