diff options
Diffstat (limited to 'Nominal/Instances')
| -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₂ |