Add EquationalReasoning combinators for _∼[ set ]_?

[jamesmckinna]

We have Function.Related.Propositional.EquationalReasoning.↔-syntax for bag equality _∼[ bag ]_, and despite _∼[ set ]_ having formally the same properties (incl. symmetry via SK-sym), we don't seem to have syntax for it (and hence the symmetric combinator syntax ↔⟨ ... ⟨ in order to be able to avoid explicit appeals to SK-sym). And AFAICT, instantiating Function.Related.Propositional.EquationalReasoning at {k = set} does not permit the ↔-syntax to be reused for set equality.

And/But I don't quite understand what needs to be changed/added to be able to fix this.

[Taneb]

I agree that this would be a reasonable addition

[MatthewDaggitt]

So the issue is that by convention we use ∼ for non-symmetric relations and so it has no symmetric counter-part. The best approach I think would be to create new BagReasoning and SetReasoning modules in List.Relation.Binary.BagAndSetEquality where we export proper (meaningfully named!) symmetric combinators...