feat(data/sym/sym2): `sym2.lift₂` (#15887)
We add `sym2.lift₂`, a two-argument version of `sym2.lift`. Its intended purpose is for defining the relation on unordered pairs relating pairs where exactly one entry decreases.
We also generalize the types for the existing `funext₂` and `funext₃`.
