Comment unused admitted results (and rename dmit -> glop).

Subset_system:
Add and prove Gen_Prod_Gen_Product.