proposition: Lemma BDDneg_memo_OK_1_2 : forall (cfg : BDDconfig) (memo : BDDneg_memo), BDDneg_memo_OK_2 cfg memo -> BDDneg_memo_OK_1 cfg memo.
proof: Proof. unfold BDDneg_memo_OK_1 in |- *. unfold BDDneg_memo_OK_2 in |- *. intros cfg memo H node node' bound H0 H1 H2. exact (proj2 (H node node' bound H1 H2)). Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4