Theorem Set.Finite.induction_on_subset

Modification history