Theorem nonempty_encodable

Modification history