Theorem Fin.orderSucc_apply

Modification history