Theorem Finset.powersetLen_succ_insert

Modification history