proposition: Lemma BDDneg_1_lemma_3 : forall (arg : BDDconfig * ad * BDDneg_memo) (x : BDDvar) (l r : ad), BDDneg_memo_lookup (snd arg) (snd (fst arg)) = None -> MapGet _ (fst (fst (fst arg))) (snd (fst arg)) = Some (x, (l, r)) -> BDDneg_1 arg 0 = (initBDDconfig, BDDzero, newMap ad).
proof: Proof. intro arg. elim arg. clear arg; intro y. elim y; clear y. intros cfg node memo x l r. intros H H0. simpl in |- *. simpl in H, H0. rewrite H. rewrite H0. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4