Theorems about `init-local` for the static soundness proof.

Some of these are actually more general and could be moved.
These more general theorems are about adding variables,
which is what `init-local` does for the local state of course.

First, we show that `add-var-value` fails iff `add-var` does
(the value put into the variable entails no constraints),
and the same holds for `add-vars-values` and `add-vars`
provided that the number of values matches the number of variables.

We prove a theorem that characterizes the effect of `init-local`
on the variable table of the computation state.
This should belong to
the theorems in theorems-about-cstate-to-vars-and-execution,
and it can probably put there, but currently it needs some other theorems,
but it may be possible to streamline and simplify its proof.

The theorem `init-local`.
This is not really a theorem about `init-local`, but it is related;
nonetheless, we may move this theorem at some point.

We finally show that `init-local` fails iff
the addition of the variables to the variable table fails,
or the number of values does not match the number of variables.

**Theorem: **

(defthm error-add-var-value-iff-error-add-var (equal (reserrp (add-var-value var val cstate)) (reserrp (add-var var (cstate-to-vars cstate)))))

**Theorem: **

(defthm error-add-vars-values-iff-error-add-vars (implies (equal (len vals) (len vars)) (equal (reserrp (add-vars-values vars vals cstate)) (reserrp (add-vars vars (cstate-to-vars cstate))))))

**Theorem: **

(defthm cstate-to-vars-of-init-local (implies (and (equal (len in-vals) (len in-vars)) (not (reserrp (init-local in-vars in-vals out-vars cstate)))) (equal (cstate-to-vars (init-local in-vars in-vals out-vars cstate)) (add-vars out-vars (add-vars in-vars nil)))))

**Theorem: **

(defthm check-var-list-when-add-vars-not-error (implies (and (identifier-listp vars) (identifier-setp varset) (not (reserrp (add-vars vars varset)))) (check-var-list vars (add-vars vars varset))))

**Theorem: **

(defthm reserrp-of-init-local (equal (reserrp (init-local in-vars in-vals out-vars cstate)) (or (reserrp (add-vars in-vars nil)) (reserrp (add-vars out-vars (add-vars in-vars nil))) (not (equal (len in-vals) (len in-vars))))))