Commit 2022-08-08 01:39 a0c5aef8

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₃.