diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-26 01:19:45 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-26 01:20:20 +0200 |
| commit | 10edba2c0365a6858a74da22042c98f9d5fa1acc (patch) | |
| tree | e8d1b29734b02cf654d91f6b33921915e108b296 /Nominal/Support.lean | |
| parent | c3700706466cb8fb9ed287ea066b656caacdc9c7 (diff) | |
simplify FPerm computations
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 |