move _≗_ from Relation.Binary.PropositionalEquality to *.Core #2331
Description
It has a very straightforward definition (if you unwind the current overly complex one) and is used a fair amount, which then drags in quite a bit more than is needed. In particular, Data.Product.Properties is otherwise very simple, but lies higher up in the dependency graph due to this single definition.