proposition: Lemma BDDneg_1_lemma_1 : forall (arg : BDDconfig * ad * BDDneg_memo) (node : ad) (bound : nat), BDDneg_memo_lookup (snd arg) (snd (fst arg)) = Some node -> BDDneg_1 arg bound = (fst (fst arg), node, snd arg).
proof: Proof. intro arg. elim arg. clear arg. intro y. elim y; clear y. intros cfg node memo node' bound. intros H. unfold BDDneg_1 in |- *. simpl in |- *. elim bound; rewrite H; simpl in |- *. reflexivity. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4