fixed opp-opp-precategory proof in Ktheory/Precategories, less weirdly