Theorem Ordinal.limitRecOn_succ

Modification history