Commit 2020-09-11 15:53 832acd63

feat(data/{sym2,sym}) decidable version of sym2.mem.other, filling out some of sym API (#4008) Removes sym2.vmem and replaces it with sym2.mem.other', which can get the other element of a pair in the presence of decidable equality. Writing sym2.mem.other' was beyond my abilities when I created sym2.vmem, and seeing that vmem is extremely specialized and has no immediate use, it's probably best to remove it. Adds some assorted simp lemmas, and also an additional lemma that sym2.mem.other is, in some sense, an involution. Adds to the API for sym. This is from taking some of the interface for multisets. (I was exploring whether sym2 α should be re-implemented as sym α 2 and trying to add enough to sym to pull it off, but it doesn't seem to be worth it in the end.) (I'm not committing a recursor for sym α n, which lets you represent elements by vectors of length n. It needs some cleanup.)