From ac2363701c3d2a03116af449ca7bc4f918fbfda7 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Fri, 24 Oct 2025 18:05:28 +0200 Subject: show properties for freshness quantifier based on equivariant relations --- Nominal/Instances/Basic.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'Nominal/Instances') diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index 82fd683..577cff8 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -38,10 +38,8 @@ instance : NominalSet 𝔸 𝔸 where simp at hc have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by intro d hd - apply Equiv.Perm.supp_notin - simp [FPerm.swap, Equiv.Perm.supp_swap, Ne.symm hc.left] - exact ⟨ne_of_mem_of_not_mem hd ha, ne_of_mem_of_not_mem hd hc.right⟩ - have h₁ : ⸨a, c⸩ • a = c := by simp [show ⸨a,c⸩ • a = (Equiv.swap a c) a from rfl] + apply FPerm.swap_neq (ne_of_mem_of_not_mem hd ha) (ne_of_mem_of_not_mem hd hc.right) + have h₁ : ⸨a, c⸩ • a = c := by rw [PermSet.atom_swap, Equiv.swap_apply_left] have h₂ : ⸨a, c⸩ • a = a := by apply hsuppS; assumption rw [h₁] at h₂ exact hc.left h₂ -- cgit v1.3.1