`*uncommitted-sapling*` is not
in the image of `pedersen`.

This was Theorem 5.4.2 in certain earlier versions of [ZPS], such as version 2020.1.0. Later versions of [ZPS] have similar theorems, but not quite the same. In any case, this property still holds, and it is proved here.

The theorem is of interest when `pedersen` returns a good hash,
which requires `pedersen-point` to return a Jubjub point.
However, since our definition of `pedersen`
returns `pedersen-point` does not return a point,
this theorem holds unconditionally.

We first prove the case in which `pedersen-point` returns a point,
and we use the definition of `*uncommitted-sapling*` in this lemma.
This is critical for
the injectivity theorem of `i2lebsp` to apply,
which reduces the goal to the inequality of
the abscissa of a Jubjub point with 1,
which is false by `jubjub-point-abscissa-is-not-1`.
The latter theorem is disabled,
but it appears that ACL2's tau system makes use of it.

**Theorem: **

(defthm pedersen-is-not-uncommitted-sapling (not (equal (pedersen d m) *uncommitted-sapling*)))