Commit 2022-07-19 01:02 00c39680

refactor(set_theory/game/pgame): tweak relabelling definition (#14941) We simplify the definition for a relabelling by using R instead of R.symm. This overall leads to more symmetric proofs. We also create a constructor with the equivalences swapped. This allows us to golf various theorems. Further, we add basic API on destructuring relabellings, which makes it so that we don't have to case on them all the time.