Theorem Set.Finite.eq_insert_of_subset_of_encard_eq_succ

Modification history