From ea38ef0cb2c57e10696c7fb6108732a6f454818c Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Thu, 20 Nov 2025 11:56:18 +0100
Subject: wip terms

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

(limited to 'Nominal/Permutations.lean')

diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index bc775b9..79a5042 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -138,6 +138,11 @@ lemma swap_mul_self {a b : X} : ⸨a, b⸩ * ⸨a, b⸩ = 1 := by
   apply ext
   simp [swap]
 
+/-- Lifting of Equiv.swap_self to finite permutations.-/
+lemma swap_self {a : X} : ⸨a, a⸩ = 1 := by
+  ext
+  simp [swap]
+
 /-- Lifting of Equiv.swap_comm to finite permutations. -/
 lemma swap_comm {a b : X} : ⸨a, b⸩ = ⸨b, a⸩ := by
   apply ext
-- 
cgit v1.3.1