Theorem Ordinal.induction

Modification history