Theorem Fin.succAbove_cases_eq_insertNth

Modification history