Add an inductive notion of equality for Data.List.Membership.Setoid

[gallais]

If we are going to deliver #432, we need an inductive notion of equality for membership
proofs. Otherwise we have to use propositional equality in lookup-injective and it only
holds for setoids whose notion of equivalence is irrelevant.

[JacquesCarette]

👍 from me. I've tried to use various bits of Data.List over Setoid, and 95% of it worked... which 100% ruined my attempts.

[gallais]

95% of it worked...

Don't hesitate to open issues for missing definitions or properties!

[JacquesCarette]

In the future, I definitely will. Unfortunately, I did that stuff 1.5 years ago, and I've forgotten exactly where things went off the rails. And for sure some of them have already been fixed.

[MatthewDaggitt]

What's the status of this? From what I understand, this is proposing defining a non-propositional equality relation over membership proofs? #432 has been closed so I assume in the end it wasn't needed?

[gallais]

#432 has been closed so I assume in the end it wasn't needed?

In the end I gave up on the generality and lookup-injective is only available
if the underlying equality of the sublist proof is propositional equality.

[MatthewDaggitt]

Thanks. This is kind of a niche result, and requires quite a lot of work so I'm going to close it for now.