Proof of Consistency Expansion (First Order Logic - Completeness)

In content/first-order-logic/completeness/henkin-expansions.tex, there is a proposition:

If $\Gamma$ is consistent in $\Lang L$ and $\Lang L'$ is obtained from $\Lang L$ by adding !!a{denumerable} set of new !!{constant}s $\Obj d_0$, $\Obj d_1$, \dots, then $\Gamma$ is consistent in~$\Lang L'$.

which doesn't have a proof. I think it should, although perhaps it could be an exercise (doesn't seem like it should be a very involved proof though).

Open content/first-order-logic/completeness/henkin-expansions.tex and read the surrounding completeness material and the proposition about adding a denumerable set of constants. Determine whether the intended resolution is a proof or an exercise, then update the proposition accordingly and verify that the surrounding LaTeX remains consistent.