Injectivity of rlp-encode-scalar, over the encodable scalars.
This is also formulated similarly to the other injectivity theorems. It readily follows from the injectivity of rlp-encode-bytes.
Theorem:
(defthm rlp-encode-scalar-injective (implies (and (not (mv-nth 0 (rlp-encode-scalar x))) (not (mv-nth 0 (rlp-encode-scalar y)))) (equal (equal (mv-nth 1 (rlp-encode-scalar x)) (mv-nth 1 (rlp-encode-scalar y))) (equal (nfix x) (nfix y)))))