proposition: Lemma BDD_EGALsymm : forall x y : BDDvar, BDDcompare x y = Datatypes.Eq -> BDDcompare y x = Datatypes.Eq.
proof: Proof. intros x y H. cut (x = y). intros H0. rewrite H0. apply BDD_EGAL_correct. assumption. apply BDD_EGAL_complete. assumption. 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