Theorem Set.iUnion_fin_add_one_eq_iUnion_succ

Modification history