start using the symmetric definition of precategory

prove being a discret precategory is a property
undo attempt to have C op op = C judgmentally

(because coq 8.3 doesn't have eta equivalence)