Theorem Fin.preimage_castSucc_Icc_castSucc

Modification history