Theorem Ordinal.type_pEmpty

Modification history