Fix eq notation instance I missed
Use \in in unique-existence notation since it uses a setoid