cousin_it comments on Inversion of theorems into definitions when generalizing