proposition: Lemma augment_eq : forall (vb : var_binding) (x : BDDvar) (b : bool), vb x = b -> var_binding_eq (augment vb x b) vb.
proof: Proof. unfold var_binding_eq in |- *. intros vb x b H x0. unfold augment in |- *. elim (sumbool_of_bool (BDDvar_eq x x0)). intro y. rewrite y. cut (x = x0). intro H0. rewrite <- H0. rewrite H; reflexivity. apply Neqb_complete. exact y. intro y. rewrite y. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2