Theorem Fin.castSuccEmb_pred_eq_pred_castSuccEmb

Modification history