proof sketch for proving different AlphaEq characterizations

1 files changed, 21 insertions, 0 deletions

diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean
index ac50519..8475a21 100644
--- a/Nominal/Equivariance.lean
+++ b/Nominal/Equivariance.lean
@@ -185,6 +185,27 @@ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸
 end Nominal
 
 /-!
+## Freshness
+
+For propositions of the form `И a, a R x`, where `R` is an equivariant relation, we do not have to differentiate between "for any fresh a" and "for all fresh a".
+-/
+section Freshness
+
+namespace Equivariance
+
+variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X}
+
+/-- The quantifier in `И a, a R x` is equivalent to "for any fresh `a`". -/
+lemma for_fresh_iff_exists : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by sorry
+
+/-- The quantifier in `И a, a R x` is equivalent to "for all fresh `a`". -/
+lemma for_fresh_iff_all : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by sorry
+
+end Equivariance
+
+end Freshness
+
+/-!
 ## Bundled Functions
 
 In the following, we also define a bundled function type for equivariant functions.