From b3f26f306945ec9e391140f1645012ba11decb40 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Mon, 27 Oct 2025 21:58:56 +0100
Subject: quotient types as nominal sets

---
 Nominal/Permutations.lean | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Nominal/Permutations.lean')

diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index a2f8d56..0d6b81c 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -158,6 +158,12 @@ lemma swap_apply_left (a b : X) : ⸨a, b⸩ a = b := by
 lemma swap_apply_right (a b : X) : ⸨a, b⸩ b = a := by
   simp [swap]
 
+/-- Lifting of Equiv.swap_inv to finite permutations. -/
+@[simp]
+lemma swap_inv (a b : X) : ⸨a, b⸩⁻¹ = ⸨a, b⸩ := by
+  apply ext
+  simp [swap]
+
 end FPerm
 
 example : FPerm ℕ := ⸨1, 2⸩ * ⸨3, 4⸩ * ⸨2, 3⸩
-- 
cgit v1.3.1