Theorem not_injective_of_ordinal_of_small

Modification history