diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 460c7ae..64cc371 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -253,7 +253,7 @@ section Freshness We also write И a, P for for_fresh (fun a => P), using the cyrillic letter И. A proposition holds for "suitably fresh" atoms iff there are infinitely many such "suitably fresh" atoms to choose from. -/ -@[simp] def NominalSet.ForFresh {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (P : 𝔸 → Prop) : Prop := +def NominalSet.ForFresh {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (P : 𝔸 → Prop) : Prop := {a : 𝔸 | P a}.Infinite macro "И" x:ident "," t:term : term => @@ -288,9 +288,16 @@ lemma fresh_exists {x : X} : ∃ (a : 𝔸), a # x := by /-- 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 - simp; intro h + simp [NominalSet.ForFresh]; intro h exact Set.Infinite.nonempty h +/-- Extensionality lemma for the freshness quantifier. -/ +lemma for_fresh_ext {P Q : 𝔸 → Prop} : (∀ a, P a ↔ Q a) → (И a, P a) = (И a, Q a) := by + intro h + simp [NominalSet.ForFresh] + suffices {a | P a} = {a | Q a} by rw [this] + exact Set.ext h + end NominalSet end Freshness |