diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 430aa8c..d80503f 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -313,7 +313,7 @@ lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ P apply PermSet.support_permutations_eq · exact supp_is_support 𝔸 · intro c hc - apply FPerm.swap_neq (ne_of_mem_of_not_mem hc ha) (ne_of_mem_of_not_mem hc hb) + apply FPerm.swap_apply_of_ne_of_ne (ne_of_mem_of_not_mem hc ha) (ne_of_mem_of_not_mem hc hb) /-- If a proposition holds for suitably fresh a, then one can always pick such an a. -/ lemma for_fresh_exists {P : 𝔸 → Prop} : (И a, P a) → (∃ a, P a) := by |