Right now we have infix:50 " ∈ " => mem in Data.List.Basic, and also a ∈ notation class Mem used for sets. I tried to replace the list notation with an instance of Mem and it broke all the proofs :-( What am I doing wrong? Obviously I could just fix all the proofs one by one and make them all longer, but I was not sure this would be welcome as a PR and I suspect I'm missing a trick.