proved that sections of restriction idempotents are a stable system of monics (up to uncomment)
	modified:   RestrictionCat.agda