proposition: Lemma BDDcompare_eq : forall x y : BDDvar, BDDcompare x y = Datatypes.Eq -> x = y.
proof: Proof. double induction x y. reflexivity. simpl in |- *. intros; discriminate. simpl in |- *. intros; discriminate. simpl in |- *. intros p p0 H. cut (p0 = p). intro H0. rewrite H0; reflexivity. apply Pcompare_Eq_eq. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps)