proposition: Lemma BDDalloc_no_new_node_1 : forall (cfg : BDDconfig) (l l1 r r1 a : ad) (x x1 : BDDvar), MapGet _ (fst (fst (BDDalloc cfg x l r))) a = Some (x1, (l1, r1)) -> (x1, (l1, r1)) = (x, (l, r)) \/ MapGet _ (fst cfg) a = Some (x1, (l1, r1)).
proof: Proof. intro cfg. elim cfg. clear cfg. intro y. intro y0. elim y0. clear y0. simpl in |- *. intro y0. intro y1. intro l. intro l1. intro r. intro r1. intro a. intro x. intro x1. rewrite (MapPut_semantics (BDDvar * (ad * ad)) y y1 (x, (l, r)) a). case (N.eqb y1 a). intro H. left. injection H. intros H0 H1 H2. rewrite H0. rewrite H1. rewrite H2. trivial. intros H. right. assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat