diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-24 18:05:28 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-24 18:05:28 +0200 |
| commit | ac2363701c3d2a03116af449ca7bc4f918fbfda7 (patch) | |
| tree | 3de16140277473558b2ad789f30ef2b7f18f26dd /Nominal/Instances/Basic.lean | |
| parent | 2489e2d5da786d6da0bda30f092c9622cc7d3f81 (diff) | |
show properties for freshness quantifier based on equivariant relations
Diffstat (limited to 'Nominal/Instances/Basic.lean')
| -rw-r--r-- | Nominal/Instances/Basic.lean | 6 |
1 files changed, 2 insertions, 4 deletions
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₂ |