Theorem List.Ico.succ_singleton

Modification history