feat(data/sym/sym2): add lemma that eq from distinct common members (#11563)
feat(data/sym/sym2): add lemma that eq from distinct common members (#11563)

Two terms of type `sym2 a` are equal if one can find two distinct elements of type `a` that are members of both.





leanprover-community/mathlib,leanprover-community/mathlib