diff options
Diffstat (limited to 'Nominal/Instances/Basic.lean')
| -rw-r--r-- | Nominal/Instances/Basic.lean | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index 2786c86..2bb389d 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -41,7 +41,7 @@ instance : NominalSet 𝔸 𝔸 where simp only [Finset.singleton_union, Finset.mem_insert, Set.Finite.mem_toFinset, not_or] at hc have hfix : ⸨a, c⸩ ∈ PermSet.fix 𝔸 S := by intro d hd - apply FPerm.swap_neq (ne_of_mem_of_not_mem hd ha) (ne_of_mem_of_not_mem hd hc.right) + apply FPerm.swap_apply_of_ne_of_ne (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₂ |